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 HaraldRuess BehzadAkbarpour HanneGottliebsen LeonvanderTorre NancyDay MikeKishinevsky TomasUribe BenDiVito HansdeNivelle Jean-ChristopheFilliatre 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...1 31 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 .

This book constitutes the proceedings of the 13th International Symposium on NASA Formal Methods, NFM 2021, held virtually in May 2021.The 21 full and 3 short papers presented in this volume were carefully reviewed and selected from 66 submissions. The papers aim to identify challenges and provide solutions to achieve assurance in mission-critical and safety-critical systems. Examples of such systems include advanced separation assurance algorithms for aircraft, next-generation air transportation, autonomous rendezvous and docking of spacecraft, on-board software for unmanned aerial systems (UAS), UAS traffic management, autonomous robots, and systems for fault detection, diagnosis, and prognostics.

This book constitutes the refereed proceedings of the 8th International Conference on Interactive Theorem Proving, ITP 2017, held in Brasilia, Brazil, in September 2017. The 28 full papers, 2 rough diamond papers, and 3 invited talk papers presented were carefully reviewed and selected from 65 submissions. The topics range from theoretical foundations to implementation aspects and applications in program verification, security and formalization of mathematical theories.

PVSio is a conservative extension to the PVS prelude library that provides basic input/output capabilities to the PVS ground evaluator. It supports rapid prototyping in PVS by enhancing the specification language with built-in constructs for string manipulation, floating point arithmetic, and input/output operations.