Typed Lambda Calculi and Applications: 4th International Conference, TLCA’99 L’Aquila, Italy, April 7–9, 1999 Proceedings

Jean-Marc Andreoli (auth.), Jean-Yves Girard (eds.)3540657630, 9783540657637

This book constitutes the refereed proceedings of the 4th International Conference on Typed Lambda Calculi and Applications, TLCA’99, held in L’Aquila, Italy in April 1999. The 25 revised full papers presented were carefully reviewed and selected from a total of 50 submissions. Also included are two invited demonstrations. The volume reports research results on various aspects of typed lambda calculi. Among the topics addressed are noncommutative logics, type theory, algebraic data types, logical calculi, abstract data types, and subtyping.

---

Table of contents :
The Coordination Language Facility and Applications….Pages 1-5
AnnoDomini in Practice: A Type-Theoretic Approach to the Year 2000 Problem….Pages 6-13
Modules in Non-commutative Logic….Pages 14-24
Elementary Complexity and Geometry of Interaction….Pages 25-33
Quantitative Semantics Revisited….Pages 40-53
Total Functionals and Well-Founded Strategies….Pages 54-68
Counting a Type’s Principal Inhabitants….Pages 69-82
Useless-Code Detection and Elimination for PCF with Algebraic Data Types….Pages 83-97
Every Unsolvable λ Term has a Decoration….Pages 98-113
Game Semantics for Untyped λβη -Calculus….Pages 114-128
A Finite Axiomatization of Inductive-Recursive Definitions….Pages 129-146
Lambda Definability with Sums via Grothendieck Logical Relations….Pages 147-161
Explicitly Typed λ μ -Calculus for Polymorphism and Call-by-Value….Pages 162-177
Soundness of the Logical Framework for Its Typed Operational Semantic….Pages 177-197
Logical Predicates for Intuitionistic Linear Type Theories….Pages 198-213
Polarized Proof-Nets: Proof-Nets for LC….Pages 213-227
Call-by-Push-Value: A Subsuming Paradigm….Pages 228-243
A Study of Abramsky’s Linear Chemical Abstract Machine….Pages 243-257
Resource Interpretations, Bunched Implications and the αλ-Calculus (Preliminary Version)….Pages 258-279
A Curry-Howard Isomorphism for Compilation and Program Execution….Pages 280-294
Natural Deduction for Intuitionistic Non-commutative Linear Logic….Pages 295-309
A Logic for Abstract Data Types as Existential Types….Pages 310-324
Characterising Explicit Substitutions which Preserve Termination….Pages 325-339
Explicit Environments….Pages 340-354
Consequences of Jacopini’s Theorem: Consistent Equalities and Equations….Pages 355-364
Strong Normalisation of Cut-Elimination in Classical Logic….Pages 365-380
Pure Type Systems with Subtyping….Pages 381-396