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 .

New concepts for automating air traffic management functions at small non-towered airports raise serious safety issues associated with the software implementations and their underlying key algorithms. The criticality of such software systems necessitates that strong guarantees of the safety be developed for them. In this paper we present a formal method for modeling and verifying such systems using the PVS theorem proving system. The method is demonstrated on a preliminary concept of operation for the Small Aircraft Transportation System (SATS) project at NASA Langley.