Types for Proofs and Programs: International Workshop, TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers (Lecture Notes in Computer Science, 1657)

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.