Theorem Proving in Higher Order Logics: 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings, Volume 15

Front Cover
Springer Science & Business Media, Aug 7, 2002 - Computers - 347 pages
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 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: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 .
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

Formal Methods at NASA Langley
1
Higher Order Unification 30 Years Later
3
Combining Higher Order Abstract Syntax with Tactical Theorem Proving and CoInduction
13
Efficient Reasoning about Executable Specifications in Coq
31
Verified Bytecode Model Checkers
47
The 5 Colour Theorem in IsabelleIsar
67
TypeTheoretic Functional Semantics
83
A Proposal for a Formal OCL Semantics in IsabelleHOL
99
Power vs Robustness
182
TwoLevel Metareasoning in Coq
198
An Example of Programming Computation and Deduction
214
A Formal Approach to Probabilistic Termination
230
Using Theorem Proving for Numerical Analysis Correctness Proof of an Automatic Differentiation Algorithm
246
A Modular Approach
263
Sequent Schema for Derived Rules
281
Algebraic Structures and Dependent Records
298

Explicit Universes for the Calculus of Constructions
115
Formalised Cut Admissibility for Display Logic
131
Formalizing the Trading Theorem for the Classification of Surfaces
148
FreeStyle Theorem Proving
164
Proving the Equivalence of Microstep and Macrostep Semantics
314
Weakest Precondition for General Recursive Programs Formalized in Coq
332
Author Index
348
Copyright

Other editions - View all

Common terms and phrases