TYPES FOR PROOFS AND PROGRAMS TYPES

INFORMALPROCEEDINGSOFTHE1993WORKSHOPONTYPESFORPROOFSANDPROGRAMS????????????????TYPESNijmegenMay1993Ed.HermanGeuversiiContentsForeword::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::ivWorkshopProgramme:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::vListofParticipants:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::viiiT.AltenkirchProvingStrongNormalizationofCCbyModifyingRealisabilitySe-mantics:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::1P.AudebaudCC+:AnextensionoftheCalculusofConstructionswithxpoints:::15F.BarbaneraandS.BerardiASymmetricLambdaCalculusfor\ClassicalProgramExtraction::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::31B.BoyerandG.DowekTowardsCheckingProof-Checkers:::::::::::::::::::::::51T.CoquandInniteObjectsinTypeTheory:::::::::::::::::::::::::::::::::::::::71T.CoquandandP.DybjerIntuitionisticModelConstructionsandNormalizationProofs::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::85T.CoquandandJ.SmithWhatisthestatusofpatternmatchingintypetheory?111G.Dowek,G.HuetandB.WernerOntheDenitionofthe-longNormalForminTypeSystemsoftheCube::::::::::::::::::::::::::::::::::::::::::::::::::::::::115H.GeuversConservativitybetweenlogicsandtypedcalculi::::::::::::::::::::::131S.HayashiLogicofrenementtypes:::::::::::::::::::::::::::::::::::::::::::::::157L.Helmink,M.SellinkandF.VaandragerProof-CheckingaDataLinkProtocol173M.HofmannEliminationofextensionalityinMartin-Loftypetheory:::::::::::::::213L.MagnussonRenementandlocalundointheinteractiveproofeditorALF::::::227S.MaharajEncodingZSchemasinTypeTheory::::::::::::::::::::::::::::::::::245M.MiculanTheExpressivePowerofStructuralOperationalSemanticswithexplicitassumptions:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::253B.NordstromTheALFproofeditor::::::::::::::::::::::::::::::::::::::::::::::285C.ParentDevelopingcertiedprogramsinthesystemCoq,TheProgramtactic::::299F.PfenningRenementTypesforLogicalFrameworks:::::::::::::::::::::::::::::315R.PollackClosureUnderAlpha-Conversion::::::::::::::::::::::::::::::::::::::::329C.RaalliMachineDeduction:::::::::::::::::::::::::::::::::::::::::::::::::::::347A.RantaTypetheoryandtheinformallanguageofmathematics:::::::::::::::::::363D.WolframSemanticsforAbstractClauses::::::::::::::::::::::::::::::::::::::::375iiiForewordThisdocumentisthepreliminaryproceedingsoftheworkshopoftheEspritBasicResearchProject6453\TypesforProofsandProgramsheldattheUniversityofNijmegen,theNether-lands,fromMay24thuntilMay28th1993.TheworkshopwasorganisedbyHenkBarendregtandHermanGeuvers.LocalarrangementsweremadebyMariellevanderZandt,ErikBarendsen,HermanGeuversandMarkRuys.TheseproceedingshavebeencollectedfromLaTEXsources,usinge-mail.Itcontains22papersfromthe35talksthatwerepresentedattheworkshop.VeryusefulsupportinsolvingtheLaTEXpuzzleswasprovidedbyErikBarendsen.ThisdocumentcanbeobtainedbyanonymousftpfromtheUniversityofNijmegen:Typeftpftp.cs.kun.nlanonymous(aslogin)[youre-mailaddress](aspassword)cd/pub/csi/CompMath/TypesbingetNijmegenTypes.ps.ZbyeivWorkshopProgrammeTypesforProofsandPrograms,Nijmegen1993MONDAY8.30Registration(andcoee)9.15WelcomeandOpening9.30Hayashi(InvitedLecture)-RepresentinglogicinATTT10.15BREAK11.00Coquand,Dybjer(Gothenburg)-MechanizedModelConstructionandNormalizationProofs11.45Altenkirch(Edinburgh)-ProvingSyntacticPropertiesoftheCalculusofConstructionsbyModifyingRealisabilityModels12.30LUNCH14.00Luo(Edinburgh)-LogicalTruthsinTypeTheory14.30Goguen(Edinburgh)-MetatheoryforaTypeTheorywithInductivetypes15.00BREAK15.30Ciszek(Edinburgh)-ALEGOproofofavariantofLangrange’stheorem16.00Aczel,Barthe(Manchester)-DevelopmentofalgebrainLEGO16.30DRINKSTUESDAY9.30Boyer(InvitedLecture)-SomerecentworkinvericationinAustin10.15BREAK10.45Helmink,Vaandrager(Eindhoven)-VerifyingandProof-Checkingacommunicationprotocol11.30Smith,Coquand(Gothenburg)-WhatisthestatusofpatternmatchinginTypeTheory?12.15Pollack(Edinburgh)-NamedandnamelessvariablesintheConstructiveEngine12.30LUNCH14.00DemosofPollackandJones(Edinburgh),Nipkow(Munich)andPfenning(Pittsburgh),15.30BREAK16.00DemosofBertot(Sophia-Antipolis),Wolfram(Oxford)andMagnussonandvonSydow(onALF)vWEDNESDAY9.30Raalli(Edinburgh)-TypeSystemforAbstractMachine10.00Loader(Oxford)-GraphandPERmodelsoflambdacalculi10.30BREAK11.00Dowek,Huet,Werner(Paris)-Onthedenitionofeta-longforminthecalculiofthecube11.30Nipkow(Munich)-AxiomaticTypeClasses12.00Bertot(SophiaAntipolis)-ProofbyPointing12.30LUNCH14.00Gardner(Edinburgh)-Thecharacterizationofcall-by-needreduction14.30Pfenning(Pittsburgh)-IntersectionTypesforLogicalFrameworks15.00BREAK15.30Dowek,Boyer(Paris,Austin)-Towardscheckingproof-checkers16.00PANELDISCUSSION19.30WORKSHOPDINNERTHURSDAY9.30Curien(InvitedLecture)-FormalParametricPolymorphism10.00Magnusson(Gothenburg)-BacktrackinginALF10.30BREAK11.00Murthy(Paris)-CPSdemystied11.45Berardi(Turin)-Asymmetriclambdacalculusfor\classicalprogramextraction12.30LUN