|
Types for Proofs and Programs: International Workshop, TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers
|
(Buch) |
Dieser Artikel gilt, aufgrund seiner Grösse, beim Versand als 2 Artikel!
Inhalt: |
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 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 . . . |
|