Willkommen, schön sind Sie da!
Logo Ex Libris

Types for Proofs and Programs

  • Kartonierter Einband
  • 220 Seiten
(0) Erste Bewertung abgeben
Bewertungen & Rezensionen
(0)
(0)
(0)
(0)
(0)
Alle Bewertungen ansehen
Thisbookcontainsaselectionofpaperspresentedatthesecondannualworkshop heldundertheauspicesoftheEspritWorkingGroup21900Types. Thewor... Weiterlesen
20%
86.00 CHF 68.80
Sie sparen CHF 17.20
Print on Demand - Auslieferung erfolgt in der Regel innert 4 bis 6 Wochen.
Bestellung & Lieferung in eine Filiale möglich

Beschreibung

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-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?cationinthePresence

Includes supplementary material: sn.pub/extras



Klappentext

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



Inhalt
On Relating Type Theories and Set Theories.- Communication Modelling and Context-Dependent Interpretation: An Integrated Approach.- Gröbner Bases in Type Theory.- A Modal Lambda Calculus with Iteration and Case Constructs.- Proof Normalization Modulo.- Proof of Imperative Programs in Type Theory.- An Interpretation of the Fan Theorem in Type Theory.- Conjunctive Types and SKInT.- Modular Structures as Dependent Types in Isabelle.- Metatheory of Verification Calculi in LEGO.- Bounded Polymorphism for Extensible Objects.- About Effective Quotients in Constructive Type Theory.- Algorithms for Equality and Unification in the Presence of Notational Definitions.- A Preview of the Basic Picture: A New Perspective on Formal Topology.

Produktinformationen

Titel: Types for Proofs and Programs
Untertitel: International Workshop, TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers
Editor:
EAN: 9783540665373
ISBN: 3540665374
Format: Kartonierter Einband
Herausgeber: Springer Berlin Heidelberg
Genre: Informatik
Anzahl Seiten: 220
Gewicht: 341g
Größe: H235mm x B155mm x T12mm
Jahr: 1999
Untertitel: Englisch
Auflage: 1999

Weitere Produkte aus der Reihe "Lecture Notes in Computer Science"