Typed Lambda Calculi and Applications

1. Front Matter

   PDF

2. A λ-to-CL translation for strong normalization

   • Yohji Akama

   Pages 1-10

3. Typed intermediate languages for shape analysis

   • Gianna Bellè, Eugenio Moggi

   Pages 11-29

4. Minimum information code in a pure functional language with data types

   • S. Berardi, L. Boerio

   Pages 30-45

5. Matching constraints for the Lambda Calculus of Objects

   • Viviana Bono, Michele Bugliesi

   Pages 46-62

6. Coinductive axiomatization of recursive type equality and subtyping

   • Michael Brandt, Fritz Henglein

   Pages 63-81

7. A simple adequate categorical model for PCF

   • Torben Braüner

   Pages 82-98

8. Logical reconstruction of bi-domains

   • Antonio Bucciarelli

   Pages 99-111

9. A module calculus for pure type systems

   • Judicaël Courant

   Pages 112-128

10. An inference algorithm for strictness

    • Ferruccio Damiani, Paola Giannini

    Pages 129-146

11. Primitive recursion for higher-order abstract syntax

    • Joëlle Despeyroux, Frank Pfenning, Carsten Schürmann

    Pages 147-163

12. Eta-expansions in dependent type theory — The calculus of constructions

    • Neil Ghani

    Pages 164-180

13. Proof nets, garbage, and computations

    • S. Guerrini, S. Martini, A. Masini

    Pages 181-195

14. Recursion from cyclic sharing: Traced monoidal categories and models of cyclic lambda calculi

    • Masahito Hasegawa

    Pages 196-213

15. Games and weak-head reduction for classical PCF

    • Hugo Herbelin

    Pages 214-230

16. A type theoretical view of Böhm-trees

    • Toshihiko Kurata

    Pages 231-247

17. Semantic techniques for deriving coinductive characterizations of observational equivalences for λ-calculi

    • Marina Lenisa

    Pages 248-266

18. Schwichtenberg-style lambda definability is undecidable

    • Jan Małolepszy, Małgorzata Moczurad, Marek Zaionc

    Pages 267-283

19. Outermost-fair rewriting

    • Femke van Raamsdonk

    Pages 284-299

20. Pomset logic: A non-commutative extension of classical linear logic

    • Christian Retoré

    Pages 300-318

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.

• Lambda calculi
• Lambda-Kalküle
• Monoid
• Programmiersprachen
• Typensysteme
• algorithm
• algorithms
• commutative property
• logic
• programming logics
• proof
• semantic techniques
• theorem proving
• type systems
• type theory

Policies and ethics