Typed Lambda Calculi and Applications: Second International Conference on Typed Lambda Calculi and Applications, TLCA ’95 Edinburgh, United Kingdom, April 10–12, 1995 Proceedings

Andrea Asperti, Cosimo Laneve (auth.), Mariangiola Dezani-Ciancaglini, Gordon Plotkin (eds.)354059048X, 9783540590484

This volume presents the proceedings of the Second International Conference on Typed Lambda Calculi and Applications, held in Edinburgh, UK in April 1995.
The book contains 29 full revised papers selected from 58 submissions and comprehensively reports the state of the art in the field. The following topics are addressed: proof theory of type systems, logic and type systems, typed lambda calculi as models of (higher-order) computation, semantics of type systems, proof verification via type systems, type systems of programming languages, and typed term rewriting systems.

---

Table of contents :
Comparing λ-calculus translations in sharing graphs….Pages 1-15
Extensions of pure type systems….Pages 16-31
A model for formal parametric polymorphism: A per interpretation for system R….Pages 32-46
A realization of the negative interpretation of the Axiom of Choice….Pages 47-62
Using subtyping in program optimization….Pages 63-77
What is a categorical model of Intuitionistic Linear Logic?….Pages 78-93
An explicit Eta rewrite rule….Pages 94-108
Extracting text from proofs….Pages 109-123
Higher-order abstract syntax in Coq….Pages 124-138
Expanding extensional polymorphism….Pages 139-153
Lambda-calculus, combinators and the comprehension scheme….Pages 154-170
βη-Equality for coproducts….Pages 171-185
Typed operational semantics….Pages 186-200
A simple calculus of exception handling….Pages 201-215
A simple model for quotient types….Pages 216-234
Untyped λ-calculus with relative typing….Pages 235-248
Final semantics for untyped λ-calculus….Pages 249-265
A simplification of Girard’s paradox….Pages 266-278
Basic properties of data types with inequational refinements….Pages 279-296
Decidable properties of intersection type systems….Pages 297-311
Termination proof of term rewriting system with the multiset path ordering. A complete development in the system Coq….Pages 312-327
Typed λ-calculi with explicit substitutions may not terminate….Pages 328-334
On equivalence classes of interpolation equations….Pages 335-349
Strict functionals for termination proofs….Pages 350-364
A verified typechecker….Pages 365-380
Categorical semantics of the call-by-value λ-calculus….Pages 381-396
A fully abstract translation between a λ-calculus with reference types and Standard ML….Pages 397-413
Categorical completeness results for the simply-typed lambda-calculus….Pages 414-427
Third-order matching in the presence of type constructors….Pages 428-442