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.

Other editions - View all