Types for Proofs and Programs - International Workshop, TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers (Paperback, 1999 ed.)

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.

General

Imprint:	Springer-Verlag
Country of origin:	Germany
Series:	Lecture Notes in Computer Science, 1657
Release date:	2001
First published:	1999
Editors:	Thorsten Altenkirch • Wolfgang Naraschewski • Bernhard Reus
Dimensions:	235 x 155 x 11mm (L x W x T)
Format:	Paperback
Pages:	212
Edition:	1999 ed.
ISBN-13:	978-3-540-66537-3
Categories:	Books > Computing & IT > General theory of computing > General Books > Computing & IT > Applications of computing > General Books > Computing & IT > Computer programming > Programming languages > General Promotions
LSN:	3-540-66537-4
Barcode:	9783540665373

Is the information for this product incomplete, wrong or inappropriate? Let us know about it.

Does this product have an incorrect or missing image? Send us a new image.

Is this product missing categories? Add more categories.

Review This Product

No reviews yet - be the first to create one!