Typed Lambda Calculi and Applications

1. Front Matter

   Pages I-XI

   PDF

2. Invited Lectures

   1. Many Happy Re urns

      • Olivier Danvy

      Pages 1-1

   2. From Bounded Arithmetic to Memory Management: Use of Type Theory to Capture Complexity Classes and Space Behaviour

      • Martin Hofmann

      Pages 2-3

   3. Definability of Total Objects in PCF and Related Calculi

      • Dag Normann

      Pages 4-5

   4. Categorical Semantics of Control

      • Peter Selinger

      Pages 6-7

3. Contributed Papers

   1. Representations of First Order Function Types as Terminal Coalgebras

      • Thorsten Altenkirch

      Pages 8-21

   2. A Finitary Subsystem of the Polymorphic λ-Calculus

      • Thorsten Altenkirch, Thierry Coquand

      Pages 22-28

   3. Sequentiality and the π-Calculus

      • Martin Berger, Kohei Honda, Nobuko Yoshida

      Pages 29-45

   4. Logical Properites of Name Restriction

      • Luca Cardelli, Andrew D. Gordon

      Pages 46-60

   5. Subtyping Recursive Games

      • Juliusz Chroboczek

      Pages 61-75

   6. Typing Lambda Terms in Elementary Logic with Linear Constraints

      • Paolo Coppola, Simone Martini

      Pages 76-90

   7. Ramied Recurrence with Dependent Types

      • Norman Danner

      Pages 91-105

   8. Game Semantics for the Pure Lazy λ-Calculus

      • Pietro Di Gianantonio

      Pages 106-120

   9. Reductions, intersection types, and explicit substitutions

      • Dan Doughertyy, Pierre Lescanne

      Pages 121-135

   10. The Stratified Foundations as a Theory Modulo

       • Gilles Dowek

       Pages 136-150

   11. Normalization by Evaluation for the Computational Lambda-Calculus

       • Andrzej Filinski

       Pages 151-165

   12. Induction Is Not Derivable in Second Order Dependent Type Theory

       • Herman Geuvers

       Pages 166-181

   13. Strong Normalization of Classical Natural Deduction with Disjunction

       • Philippe de Groote

       Pages 182-196

   14. Partially Additive Categories and Fully Complete Models of Linear Logic

       • Esfandiar Haghverdi

       Pages 197-216

   15. Distinguishing Data Structures and Functions: The Constructor Calculus and Functorial Types

       • C. Barry Jay

       Pages 217-239

This book constitutes the refereed proceedings of the 5th International Conference on Typed Lambda Calculi and Applications, TLCA 2001, held in Krakow, Poland in May 2001. The 28 revised full papers presented were carefully reviewed and selected from 55 submissions. The volume reports research results on all current aspects of typed lambda calculi. Among the topics addressed are type systems, subtypes, coalgebraic methods, pi-calculus, recursive games, various types of lambda calculi, reductions, substitutions, normalization, linear logic, cut-elimination, prelogical relations, and mu calculus.

• categorical methods
• computational logic
• deduction
• lambda calculi
• lambda calculus
• logic
• logical relations
• program logics
• program semantics
• programming theory
• type systems
• typed lambda calculi

• Oxford University Computing Laboratory, Oxford, USA

  Samson Abramsky

Policies and ethics