Typed lambda calculi and applications : Third International Conference on Typed Lambda Calculi and Applications, TLCA '97, Nancy, France, April 2-4, 1997 : proceedings

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

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.

We often find some translations from -calculus to combinatory logic (CL) provide a pleasing viewpoint in the study of -calculus.