Buch, Englisch, Band 1657, 212 Seiten, Format (B × H): 155 mm x 235 mm, Gewicht: 341 g
International Workshop, TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers
Buch, Englisch, Band 1657, 212 Seiten, Format (B × H): 155 mm x 235 mm, Gewicht: 341 g
Reihe: Lecture Notes in Computer Science
ISBN: 978-3-540-66537-3
Verlag: Springer Berlin Heidelberg
WolfgangNaraschewski BernhardReus VI List of Referees PeterAczel PetriMäenp¨ä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 Jö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-Löf’sconstructive typetheory,[13]. Intuitivelythereisaneasywaytodetermineanupperbound ontheprooftheoreticstrength. Thisistousethe‘obvious’types-as-sets- terpretation of these type theories in a strong enough classical axiomatic set theory.
Zielgruppe
Research
Autoren/Hrsg.
Fachgebiete
- Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Prozedurale Programmierung
- Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Programmier- und Skriptsprachen
- Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Programmierung: Methoden und Allgemeines
- Mathematik | Informatik EDV | Informatik Informatik Künstliche Intelligenz Wissensbasierte Systeme, Expertensysteme
Weitere Infos & Material
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.
