César A. Muñoz – författare
Visar alla böcker från författaren César A. Muñoz. Handla med fri frakt och snabb leverans.
3 produkter
3 produkter
NASA Formal Methods
13th International Symposium, NFM 2021, Virtual Event, May 24–28, 2021, Proceedings
Häftad, Engelska, 2021
914 kr
Skickas inom 10-15 vardagar
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.
Del 10499 - Lecture Notes in Computer Science
Interactive Theorem Proving
8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings
Häftad, Engelska, 2017
557 kr
Skickas inom 10-15 vardagar
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.
Theorem Proving in Higher Order Logics
15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings
Häftad, Engelska, 2002
559 kr
Skickas inom 10-15 vardagar
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...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 .