Types for Proofs and Programs

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.