Types for Proofs and Programs: International Workshop, TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers: 1657 - Brossura

Altenkirch, Thorsten; Naraschewski, Wolfgang; Reus, Bernhard

Brossura

ISBN 10: 3540665374 ISBN 13: 9783540665373

Casa editrice: Springer, 2008

Riassunto

WolfgangNaraschewski BernhardReus VI List of Referees PeterAczel PetriMa¨enp¨a¨a ThorstenAltenkirch RalphMatthes GillesBarthe MichaelMendler HenkBarendregt WolfgangNaraschewski UliBerger TobiasNipkow MarcBezem SaraNegri VenanzioCapretta ChristinePaulin-Mohring MarioCoppo HenrikPersson CatarinaCoquand RandyPollack RobertoDiCosmo DavidPym GillesDowek ChristopheRa?alli MarcDymetman AarneRanta Jean-ChristopheFilli atre BernhardReus NeilGhani EikeRitter MartinHofmann GiovanniSambin MonikaSeisenberger FurioHonsell AntonSetzer PaulJackson JanSmith FelixJoachimski FlorianKammuller ¨ SergeiSoloview JamesMcKinna MakotoTakeyama Sim aoMelodeSousa SilvioValentini ThomasKleymann MarkusWenzel HansLeiss BenjaminWerner Table of Contents OnRelatingTypeTheoriesandSetTheories. . . . . . . . . . . . . . . . . . . . . . . . . . 1 PeterAczel CommunicationModellingandContext-DependentInterpretation: AnIntegratedApproach. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 Ren´eAhn,TijnBorghuis Grobner ¨ BasesinTypeTheory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ThierryCoquand,HenrikPersson AModalLambdaCalculuswithIterationandCaseConstructs. . . . . . . . . . 47 Jo¨elleDespeyroux,PierreLeleu ProofNormalizationModulo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 GillesDowek,BenjaminWerner ProofofImperativeProgramsinTypeTheory. . . . . . . . . . . . . . . . . . . . . . . . . 78 Jean-ChristopheFilli atre AnInterpretationoftheFanTheoreminTypeTheory . . . . . . . . . . . . . . . . . 93 DanielFridlender ConjunctiveTypesandSKInT. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106 JeanGoubault-Larrecq ModularStructuresasDependentTypesinIsabelle . . . . . . . . . . . . . . . . . . . . 121 FlorianKammul ¨ler MetatheoryofVeri?cationCalculiinLEGO. . . . . . . . . . . . . . . . . . . . . . . . . . . 133 ThomasKleymann BoundedPolymorphismforExtensibleObjects . . . . . . . . . . . . . . . . . . . . . . . . 149 LuigiLiquori AboutE?ectiveQuotientsinConstructiveTypeTheory . . . . . . . . . . . . . . . . 164 MariaEmiliaMaietti VIII AlgorithmsforEqualityandUni?cationinthePresenceof NotationalDe?nitions. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 179 FrankPfenning,CarstenSch¨urmann APreviewoftheBasicPicture:ANewPerspectiveonFormalTopology. . 194 GiovanniSambin,SilviaGebellato On Relating TypeTheories and Set Theories PeterAczel Departments of Mathematics and Computer Science Manchester University petera@cs. man. ac. uk Introduction 1 The original motivation for the work described in this paper was to det- minetheprooftheoreticstrengthofthetypetheoriesimplementedintheproof developmentsystemsLegoandCoq,[12,4]. Thesetypetheoriescombinetheim- 2 predicativetype of propositions , from the calculus of constructions,[5], with theinductivetypesandhierarchyoftypeuniversesofMartin-Lo¨f sconstructive typetheory,[13]. Intuitivelythereisaneasywaytodetermineanupperbound ontheprooftheoreticstrength. Thisistousethe obvious types-as-sets- terpretation of these type theories in a strong enough classical axiomatic set theory.

Su questo libro

Contenuti

On Relating Type Theories and Set Theories.- Communication Modelling and Context-Dependent Interpretation: An Integrated Approach.- Gröbner Bases in Type Theory.- A Modal Lambda Calculus with Iteration and Case Constructs.- Proof Normalization Modulo.- Proof of Imperative Programs in Type Theory.- An Interpretation of the Fan Theorem in Type Theory.- Conjunctive Types and SKInT.- Modular Structures as Dependent Types in Isabelle.- Metatheory of Verification Calculi in LEGO.- Bounded Polymorphism for Extensible Objects.- About Effective Quotients in Constructive Type Theory.- Algorithms for Equality and Unification in the Presence of Notational Definitions.- A Preview of the Basic Picture: A New Perspective on Formal Topology.

Dettagli dell'edizione

• Editore: Springer
• Data di pubblicazione: 2008
• Lingua: Inglese
• ISBN 10: 3540665374
• ISBN 13: 9783540665373
• Rilegatura: Copertina flessibile
• Numero di pagine: 220
• Contatto del produttore: GPSR Kontakt; ProductSafety@springernature.com; ; Slevogtstraße 3-5; Heidelberg; 69126; Germania