Typed Lambda Calculi and Applications: 5th International Conference, TLCA 2001 Kraków, Poland, May 2–5, 2001 Proceedings

Olivier Danvy (auth.), Samson Abramsky (eds.)3540419608, 9783540419600

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.

---

Table of contents :
Many Happy Re urns….Pages 1-1
From Bounded Arithmetic to Memory Management: Use of Type Theory to Capture Complexity Classes and Space Behaviour….Pages 2-3
Definability of Total Objects in PCF and Related Calculi….Pages 4-5
Categorical Semantics of Control….Pages 6-7
Representations of First Order Function Types as Terminal Coalgebras….Pages 8-21
A Finitary Subsystem of the Polymorphic λ-Calculus….Pages 22-28
Sequentiality and the π-Calculus….Pages 29-45
Logical Properites of Name Restriction….Pages 46-60
Subtyping Recursive Games….Pages 61-75
Typing Lambda Terms in Elementary Logic with Linear Constraints….Pages 76-90
Ramied Recurrence with Dependent Types….Pages 91-105
Game Semantics for the Pure Lazy λ-Calculus….Pages 106-120
Reductions, intersection types, and explicit substitutions….Pages 121-135
The Stratified Foundations as a Theory Modulo….Pages 136-150
Normalization by Evaluation for the Computational Lambda-Calculus….Pages 151-165
Induction Is Not Derivable in Second Order Dependent Type Theory….Pages 166-181
Strong Normalization of Classical Natural Deduction with Disjunction….Pages 182-196
Partially Additive Categories and Fully Complete Models of Linear Logic….Pages 197-216
Distinguishing Data Structures and Functions: The Constructor Calculus and Functorial Types….Pages 217-239
The Finitely Generated Types of the λ-Calculus….Pages 240-252
Deciding Monadic Theories of Hyperalgebraic Trees….Pages 253-267
A Deconstruction of Non-deterministic Classical Cut Elimination….Pages 268-282
A Token Machine for Full Geometry of Interaction (Extended Abstract)….Pages 283-297
Second-Order Pre-logical Relations and Representation Independence….Pages 298-314
Characterizing Convergent Terms in Object Calculi via Intersection Types….Pages 315-328
Parigot’s Second Order λ μ -Calculus and Inductive Types….Pages 329-343
The Implicit Calculus of Constructions Extending Pure Type Systems with an Intersection Type Binder and Subtyping….Pages 344-359
Evolving Games and Essential Nets for Affine Polymorphism….Pages 360-375
Retracts in Simple Types….Pages 376-384
Parallel Implementation Models for the λ-Calculus Using the Geometry of Interaction (Extended Abstract)….Pages 385-399
The complexity of β-reduction in low orders….Pages 400-414
Strong Normalisation for a Gentzen-like Cut-Elimination Procedure….Pages 415-429