Theorem Proving In Higher Order Logics: 15th International Conference, Tphols 2002, Hampton, Va, Usa, August 20-23, 2002. Proceedings (lecture Notes In Computer Science)

This book constitutes the refereed proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2002, held in Hampton, VA, USA in August 2002. The 20 revised full papers presented together with 2 invited contributions were carefully reviewed and selected from 34 submissions. All current issues in HOL theorem proving and formal verification of software and hardware systems are addressed. Among the HOL theorem proving systems evaluated are Isabelle/HOL, Isabelle/Isar, and Coq. Formal Methods at NASA Langley....Pages 1-2 Higher Order Unification 30 Years Later....Pages 3-12 Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction....Pages 13-30 Efficient Reasoning about Executable Specifications in Coq....Pages 31-46 Verified Bytecode Model Checkers....Pages 47-66 The 5 Colour Theorem in Isabelle/Isar....Pages 67-82 Type-Theoretic Functional Semantics....Pages 83-97 A Proposal for a Formal OCL Semantics in Isabelle/HOL....Pages 99-114 Explicit Universes for the Calculus of Constructions....Pages 115-130 Formalised Cut Admissibility for Display Logic....Pages 131-147 Formalizing the Trading Theorem for the Classification of Surfaces....Pages 148-163 Free-Style Theorem Proving....Pages 164-181 A Comparison of Two Proof Critics: Power vs. Robustness....Pages 182-197 Two-Level Meta-reasoning in Coq....Pages 198-213 PuzzleTool: An Example of Programming Computation and Deduction....Pages 214-229 A Formal Approach to Probabilistic Termination....Pages 230-245 Using Theorem Proving for Numerical Analysis Correctness Proof of an Automatic Differentiation Algorithm....Pages 246-262 Quotient Types: A Modular Approach....Pages 263-280 Sequent Schema for Derived Rules....Pages 281-297 Algebraic Structures and Dependent Records....Pages 298-313 Proving the Equivalence of Microstep and Macrostep Semantics....Pages 314-331 Weakest Precondition for General Recursive Programs Formalized in Coq....Pages 332-347 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 HaraldRueß BehzadAkbarpour HanneGottliebsen LeonvanderTorre NancyDay MikeKishinevsky TomasUribe BenDiVito HansdeNivelle Jean-ChristopheFilliˆatre AndrewPitts Invited Speakers 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 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 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 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 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. ... ... .. 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

this Book Constitutes The Refereed Proceedings Of The 15th International Conference On Theorem Proving In Higher Order Logics, Tphols 2002, Held In Hampton, Va, Usa In August 2002.
the 20 Revised Full Papers Presented Together With 2 Invited Contributions Were Carefully Reviewed And Selected From 34 Submissions. All Current Issues In Hol Theorem Proving And Formal Verification Of Software And Hardware Systems Are Addressed. Among The Hol Theorem Proving Systems Evaluated Are Isabelle/hol, Isabelle/isar, And Coq.