Theorem Proving in Higher Order Logics

15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings
Erscheinungsjahr 2002
ISBN: 978-3-540-44039-0
Verlag: Springer

Buch, Englisch, 347 Seiten, Format (B × H): 155 mm x 235 mm, Gewicht: 1130 g

Reihe: Lecture Notes in Computer Science

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 Judicä 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.

Zielgruppe

Research

Autoren/Hrsg.

Carreno, Victor A.

Munoz, Cesar A.

Tahar, Sofiene

Fachgebiete

• Mathematik | Informatik EDV | Informatik Informatik Rechnerarchitektur
• Mathematik | Informatik EDV | Informatik Informatik Mathematik für Informatiker
• Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Software Engineering Objektorientierte Softwareentwicklung
• Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Programmierung: Methoden und Allgemeines

Inhaltsverzeichnis

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.