Theorem Proving in Higher Order Logics

Thisvolumecontainstheproceedingsofthe 15th International Conference on TheoremProvinginHigherOrderLogics(TPHOLs2002)heldon20-23August 2002inHampton,Virginia,USA. Theconferenceservesasavenueforthep- sentationofworkintheoremprovinginhigher-orderlogics,andrelatedareas indeduction,formalspeci?cation,softwareandhardwareveri?cation,andother applications. Eachofthe34paperssubmittedinthefullresearchcategorywasrefereedby atleastthreereviewersfromtheprogramcommitteeorbyareviewerappointed bytheprogramcommittee. Ofthesesubmissions,20paperswereacceptedfor presentationattheconferenceandpublicationinthisvolume. Followingawell-establishedtraditioninthisconferenceseries,TPHOLs2002 alsoo?eredavenueforthepresentationofworkinprogress. Fortheworkin progresstrack,shortintroductorytalksweregivenbyresearchers,followedby anopenpostersessionforfurtherdiscussion. Papersacceptedforpresentation inthistrackhavebeenpublishedasConferenceProceedingsCPNASA-2002- 211736. TheorganizerswouldliketothankRickyButlerandG'erardHuetforgra- fullyacceptingourinvitationtogivetalksatTPHOLs2002. RickyButlerwas instrumentalintheformationoftheFormalMethodsprogramattheNASA LangleyResearchCenterandhasledthegroupsinceitsbeginnings.TheNASA LangleyFormalMethodsgroup,underRickyButler'sguidance,hasfunded, beeninvolvedin,orin?uencedmanyformalveri?cationprojectsintheUSover morethantwodecades. In1998G'erardHuetreceivedtheprestigiousHerbrand Awardforhisfundamentalcontributionstotermrewritingandtheoremproving inhigher-orderlogic,aswellasmanyotherkeycontributionstothe?eldof- tomatedreasoning. HeistheoriginatoroftheCoqSystem,underdevelopment atINRIA-Rocquencourt. Dr. Huet'scurrentmaininterestiscomputationall- guistics,howeverhisworkcontinuestoin?uenceresearchersaroundtheworldin awidespectrumofareasintheoreticalcomputerscience,formalmethods,and softwareengineering. ThevenueoftheTPHOLsconferencetraditionallychangescontinenteach yearinordertomaximizethelikelihoodthatresearchersfromallovertheworld willattend.Startingin1993,theproceedingsofTPHOLsanditspredecessor workshopshavebeenpublishedinthefollowingvolumesoftheSpringer-Verlag LectureNotesinComputerScienceseries: 1993(Canada) 780 1998(Australia)1479 1994(Malta) 859 1999(France) 1690 1995(USA) 971 2000(USA) 1869 1996(Finland)1125 2001(UK) 2152 1997(USA) 1275 VI Preface The2002conferencewasorganizedbyateamfromNASALangleyResearch Center,theICASEInstituteatLangleyResearchCenter,andConcordiaU- versity. FinancialsupportcamefromIntelCorporation. Thesupportofallthese organizationsisgratefullyacknowledged. August2002 V'?ctorA. Carreno " C'esarA. Muno "z VII Organization TPHOLs2002isorganizedbyNASALangleyandICASEincooperationwith ConcordiaUniversity. Organizing Committee ConferenceChair: V'?ctorA. Carren"o(NASALangley) ProgramChair: C'esarA. Muno "z(ICASE,NASALaRC) So?'eneTahar(ConcordiaUniversity) ProgramCommittee MarkAagaard(Waterloo) MichaelKohlhase(CMU&Saarland) DavidBasin(Freiburg) ThomasKropf(Bosch) V'?ctorCarren"o(NASALangley) TomMelham(Glasgow) Shiu-KaiChin(Syracuse) JStrotherMoore(Texas,Austin) PaulCurzon(Middlesex) C'esarMuno "z(ICASE,NASALaRC) GillesDowek(INRIA) SamOwre(SRI) HaraldGanzinger(MPISaarbruc ken) ChristinePaulin-Mohring(INRIA) GaneshGopalakrishnan(Utah) LawrencePaulson(Cambridge) JimGrundy(Intel) FrankPfenning(CMU) ElsaGunter(NJIT) KlausSchneider(Karlsruhe) JohnHarrison(Intel) HennySipma(Stanford) DougHowe(Carleton) KonradSlind(Utah) BartJacobs(Nijmegen) DonSyme(Microsoft) PaulJackson(Edinburgh) So?'eneTahar(Concordia) SaraKalvala(Warwick) WaiWong(HongKongBaptist) Additional Reviewers OtmaneAit-Mohamed AlfonsGeser HaraldRuess BehzadAkbarpour HanneGottliebsen LeonvanderTorre NancyDay MikeKishinevsky TomasUribe BenDiVito HansdeNivelle Jean-ChristopheFilliatre AndrewPitts Invited Speakers RickyButler(NASALangley) G'erardHuet(INRIA) VIII Preface Sponsoring Institutions NASALangley ICASE ConcordiaUniversity INTEL Table of Contents Invited Talks FormalMethodsatNASALangley...1 RickyButler HigherOrderUni?cation30YearsLater...3 G' erardHuet Regular Papers CombiningHigherOrderAbstractSyntaxwithTacticalTheoremProving and(Co)Induction ...13 Simon J. Ambler,RoyL. Crole,AlbertoMomigliano E?cientReasoningaboutExecutableSpeci?cationsinCoq...31 GillesBarthe,PierreCourtieu Veri?edBytecodeModelCheckers...47 DavidBasin,StefanFriedrich,MarekGawkowski The5ColourTheoreminIsabelle/Isar...67 GertrudBauer,TobiasNipkow Type-TheoreticFunctionalSemantics...83 YvesBertot,VenanzioCapretta,KuntalDasBarman AProposalforaFormalOCLSemanticsinIsabelle/HOL...99 AchimD. Brucker,BurkhartWol? ExplicitUniversesfortheCalculusofConstructions...115 Judica. elCourant FormalisedCutAdmissibilityforDisplayLogic...131 JeremyE. Dawson,RajeevGor'e FormalizingtheTradingTheoremfortheClassi?cationofSurfaces...148 ChristopheDehlinger,Jean-Fran,coisDufourd Free-StyleTheoremProving...164 DavidDelahaye AComparisonofTwoProofCritics:Powervs. Robustness...182 LouiseA. Dennis,AlanBundy X TableofContents Two-LevelMeta-reasoninginCoq...198 AmyP. Felty PuzzleTool:AnExampleofProgrammingComputationandDeduction . . 214 MichaelJ. C. Gordon AFormalApproachtoProbabilisticTermination...230 JoeHurd UsingTheoremProvingforNumericalAnalysis...246 MicaelaMayero QuotientTypes:AModularApproach...263 AlekseyNogin SequentSchemaforDerivedRules ...281 AlekseyNogin,JasonHickey AlgebraicStructuresandDependentRecords ...298 VirgilePrevosto,DamienDoligez,Th' er' eseHardin ProvingtheEquivalenceofMicrostepandMacrostepSemantics...314 KlausSchneider WeakestPreconditionforGeneralRecursiveProgramsFormalizedinCoq .