Anglický jazyk

Types for Proofs and Programs

Na objednávku

52.24 €

bežná cena: 54.99 €

O knihe

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 . . .