Research Catalog

Title

Typed lambda calculi and applications : Second International Conference on Typed Lambda Calculi and Applications, TLCA '95, Edinburgh, United Kingdom, April 10-12, 1995 : proceedings / Mariangiola Dezani-Ciancaglini, Gordon Plotkin (eds.).

Author

International Conference on Typed Lambda Calculi and Applications (2nd : 1995 : Edinburgh, Scotland)

Publication

Berlin ; New York : Springer-Verlag, [1995], ©1995.

Items in the Library & Off-site

Holdings

Details

Additional Authors

• Dezani-Ciancaglini, M. (Mariangiola)
• Plotkin, G. (Gordon), 1946-

Description

viii, 442 pages : illustrations; 24 cm.

Series Statement

Lecture notes in computer science ; 902

Uniform Title

Lecture notes in computer science ; 902.

Subject

• Lambda calculus > Congresses

Bibliography (note)

• Includes bibliographical references.

Contents

• Comparing [lambda]-calculus translations in sharing graphs / A. Asperti and C. Laneve -- Extensions of pure type systems / G. Barthe -- A model for formal parametric polymorphism: a PER interpretation for system R / R. Bellucci, M. Abadi and P.-L. Curien -- A realization of the negative interpretation of the Axiom of Choice / S. Berardi, M. Bezem and T. Coquand -- Using subtyping in program optimization / S. Berardi and L. Boerio -- What is a categorical model of intuitionistic linear logic? / G. M. Bierman -- An explicit Eta rewrite rule / D. Briaud -- Extracting text from proofs / Y. Coscoy, G. Kahn and L. Thery -- Higher-order abstract syntax in Coq / J. Despeyroux, A. Felty and A. Hirschowitz -- Expanding extensional polymorphism / R. Di Cosmo and A. Piperno -- Lambda-calculus, combinators and the comprehension scheme / G. Dowek -- [beta][eta]-equality for coproducts / N. Ghani -- Typed operational semantics / H. Goguen -- A simple calculus of exception handling / P. de Groote.
• A simple model for quotient types / M. Hofmann -- Untyped [lambda]-calculus with relative typing / M. R. Holmes -- Final semantics for untyped [lambda]-calculus / F. Honsell and M. Lenisa -- A simplification of Girard's paradox / A. J. C. Hurkens -- Basic properties of data types with inequational refinements / H. Kondoh -- Decidable properties of intersection type systems / T. Kurata and M. Takahashi -- Termination proof of term rewriting system with the multiset path ordering. A complete development in the system Coq / F. Leclerc -- Typed [lambda]-calculi with explicit substitutions may not terminate / P. A. Mellies -- On equivalence classes of interpolation equations / V. Padovani -- Strict functionals for termination proofs / J. van de Pol and H. Schwichtenberg -- A verified typechecker / R. Pollack -- Categorical semantics of the call-by-value [lambda]-calculus / A. Pravato, S. Ronchi della Rocca and L. Roversi.
• A fully abstract translation between a [lambda]-calculus with reference types and standard ML / E. Ritter and A. M. Pitts -- Categorical completeness results for the simply-typed [lambda]-calculus / A. K. Simpson -- Third-order matching in the presence of type constructors / J. Springintveld.

ISBN

• 354059048X (Berlin : softcover : acid-free) :
• 038759048X (New York : softcover : acid-free)

LCCN

95005969

OCLC

ocm32014143

Owning Institutions

Columbia University Libraries