Theorem Proving in Higher Order Logics: 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings (Lecture Notes in Computer Science, 2410). Questo articolo non è disponibile.Theorem Proving in Higher Order Logics: 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings (Lecture Notes in Computer Science, 2410)

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 HaraldRueß BehzadAkbarpour HanneGottliebsen LeonvanderTorre NancyDay MikeKishinevsky TomasUribe BenDiVito HansdeNivelle Jean-ChristopheFilliˆatre 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:AnExampleofProgrammi

Invited Talks.- Formal Methods at NASA Langley.- Higher Order Unification 30 Years Later.- Regular Papers.- Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction.- Efficient Reasoning about Executable Specifications in Coq.- Verified Bytecode Model Checkers.- The 5 Colour Theorem in Isabelle/Isar.- Type-Theoretic Functional Semantics.- A Proposal for a Formal OCL Semantics in Isabelle/HOL.- Explicit Universes for the Calculus of Constructions.- Formalised Cut Admissibility for Display Logic.- Formalizing the Trading Theorem for the Classification of Surfaces.- Free-Style Theorem Proving.- A Comparison of Two Proof Critics: Power vs. Robustness.- Two-Level Meta-reasoning in Coq.- PuzzleTool: An Example of Programming Computation and Deduction.- A Formal Approach to Probabilistic Termination.- Using Theorem Proving for Numerical Analysis Correctness Proof of an Automatic Differentiation Algorithm.- Quotient Types: A Modular Approach.- Sequent Schema for Derived Rules.- Algebraic Structures and Dependent Records.- Proving the Equivalence of Microstep and Macrostep Semantics.- Weakest Precondition for General Recursive Programs Formalized in Coq.