Typed Lambda Calculi and Applications: Third International Conference on Typed Lambda Calculi and Applications TLCA ’97 Nancy, France, April 2–4, 1997 Proceedings

Yohji Akama (auth.), Philippe de Groote, J. Roger Hindley (eds.)3540626883, 9783540626886

This book constitutes the refereed proceedings of the Third International Conference on Typed Lambda Calculi and Applications, TLCA ’97, held in Nancy, France, in April 1997.
The 24 revised full papers presented in the book were carefully selected from a total of 54 submissions. The book reports the main research advances achieved in the area of typed lambda calculi since the predecessor conference, held in 1995, and competently reflects the state of the art in the area.

---

Table of contents :
A λ-to-CL translation for strong normalization….Pages 1-10
Typed intermediate languages for shape analysis….Pages 11-29
Minimum information code in a pure functional language with data types….Pages 30-45
Matching constraints for the Lambda Calculus of Objects….Pages 46-62
Coinductive axiomatization of recursive type equality and subtyping….Pages 63-81
A simple adequate categorical model for PCF….Pages 82-98
Logical reconstruction of bi-domains….Pages 99-111
A module calculus for pure type systems….Pages 112-128
An inference algorithm for strictness….Pages 129-146
Primitive recursion for higher-order abstract syntax….Pages 147-163
Eta-expansions in dependent type theory — The calculus of constructions….Pages 164-180
Proof nets, garbage, and computations….Pages 181-195
Recursion from cyclic sharing: Traced monoidal categories and models of cyclic lambda calculi….Pages 196-213
Games and weak-head reduction for classical PCF….Pages 214-230
A type theoretical view of Böhm-trees….Pages 231-247
Semantic techniques for deriving coinductive characterizations of observational equivalences for λ-calculi….Pages 248-266
Schwichtenberg-style lambda definability is undecidable….Pages 267-283
Outermost-fair rewriting….Pages 284-299
Pomset logic: A non-commutative extension of classical linear logic….Pages 300-318
Computational reflection in the calculus of constructions and its application to theorem proving….Pages 319-335
Names, equations, relations: Practical ways to reason about new ….Pages 336-353
An axiomatic system of parametricity….Pages 354-372
Inhabitation in typed lambda-calculi (a syntactic approach)….Pages 373-389
Weak and strong beta normalisations in typed λ-calculi….Pages 390-404