Types for Proofs and Programs
International Workshop, TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers
Published on 22. September 1999
Book
Paperback/Softback
VIII, 212 pages
978-3-540-66537-3 (ISBN)
Description
Thisbookcontainsaselectionofpaperspresentedatthesecondannualworkshop heldundertheauspicesoftheEspritWorkingGroup21900Types. Theworkshop tookplaceinIrsee,Germany,from27to31ofMarch1998andwasattendedby 89researchers. Ofthe25submissions,14wereselectedforpublicationafteraregularref- eeingprocess. The?nalchoicewasmadebytheeditors. Thisvolumeisasequeltotheproceedingsfromthe?rstworkshopofthe workinggroup,whichtookplaceinAussois,France,inDecember1996. The proceedingsappearedinvol. 1512oftheLNCSseries,editedbyChristinePaulin- MohringandEduardoGim'enez. Theseworkshopsare,inturn,acontinuationofthemeetingsorganizedin 1993,1994,and1995undertheauspicesoftheEspritBasicResearchAction 6453 Types for Proofs and Programs. Thoseproceedingswerealsopublished intheLNCSseries,editedbyHenkBarendregtandTobiasNipkow(vol. 806, 1993),byPeterDybjer,BengtNordstr..omandJanSmith(vol. 996,1994)and byStefanoBerardiandMarioCoppo(vol. 1158,1995). TheEspritBRA6453 wasacontinuationoftheformerEspritAction3245Logical Frameworks: - sign,ImplementationandExperiments.
Thearticlesfromtheannualworkshops organizedunderthatActionwereeditedbyGerardHuetandGordonPlotkin inthebooksLogical FrameworksandLogicalEnvironments,bothpublishedby CambridgeUniversityPress. Acknowledgments WewouldliketothankIrmgardMignaniandAgnesSzabo-Lackingerforhelping uswithprocessingtheregistrations,andRalphMatthesandMarkusWenzelfor organizationalsupportduringthemeeting. Weareindebtedtotheorganizersof theWorkingGroupTypesandalsotoPeterClote,TobiasNipkowandMartin Wirsingforgivingustheopportunitytoorganizethisworkshopandfortheir support. WewouldalsoliketoacknowledgefundingbytheEuropeanUnion. Thisvolumewouldnothavebeenpossiblewithouttheworkofthereferees. Theyarelistedonthenextpageandwethankthemfortheirinvaluablehelp. June1999 ThorstenAltenkirch 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-ChristopheFilliatre 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-ChristopheFilliatre 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.
Thearticlesfromtheannualworkshops organizedunderthatActionwereeditedbyGerardHuetandGordonPlotkin inthebooksLogical FrameworksandLogicalEnvironments,bothpublishedby CambridgeUniversityPress. Acknowledgments WewouldliketothankIrmgardMignaniandAgnesSzabo-Lackingerforhelping uswithprocessingtheregistrations,andRalphMatthesandMarkusWenzelfor organizationalsupportduringthemeeting. Weareindebtedtotheorganizersof theWorkingGroupTypesandalsotoPeterClote,TobiasNipkowandMartin Wirsingforgivingustheopportunitytoorganizethisworkshopandfortheir support. WewouldalsoliketoacknowledgefundingbytheEuropeanUnion. Thisvolumewouldnothavebeenpossiblewithouttheworkofthereferees. Theyarelistedonthenextpageandwethankthemfortheirinvaluablehelp. June1999 ThorstenAltenkirch 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-ChristopheFilliatre 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-ChristopheFilliatre 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.
More details
Series
Edition
1999 ed.
Language
English
Place of publication
Berlin
Germany
Publishing group
Springer Berlin
Target group
Professional and scholarly
Research
Illustrations
VIII, 212 p.
Dimensions
Height: 235 mm
Width: 155 mm
Thickness: 13 mm
Weight
341 gr
ISBN-13
978-3-540-66537-3 (9783540665373)
DOI
10.1007/3-540-48167-2
Schweitzer Classification
Other editions
Additional editions
Thorsten Altenkirch | Wolfgang Naraschewski | Bernhard Reus
Types for Proofs and Programs
International Workshop, TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers
E-Book
06/2003
Springer
€53.49
Available for download
Content
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.