Typed lambda calculi and applications : 5th international conference, TLCA 2001, Kraków, Poland, May 2-5, 2001 : proceedings

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. 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 Typed Lambda Calculi and Applications: 5th International Conference, TLCA 2001 Kraków, Poland, May 2–5, 2001 Proceedings Author: Samson Abramsky Published by Springer Berlin Heidelberg ISBN: 978-3-540-41960-0 DOI: 10.1007/3-540-45413-6 Table of Contents: Many Happy Re urns From Bounded Arithmetic to Memory Management: Use of Type Theory to Capture Complexity Classes and Space Behaviour Definability of Total Objects in PCF and Related Calculi Categorical Semantics of Control Representations of First Order Function Types as Terminal Coalgebras A Finitary Subsystem of the Polymorphic λ-Calculus Sequentiality and the π-Calculus Logical Properites of Name Restriction Subtyping Recursive Games Typing Lambda Terms in Elementary Logic with Linear Constraints Ramied Recurrence with Dependent Types Game Semantics for the Pure Lazy λ-Calculus Reductions, intersection types, and explicit substitutions The Stratified Foundations as a Theory Modulo Normalization by Evaluation for the Computational Lambda-Calculus Induction Is Not Derivable in Second Order Dependent Type Theory Strong Normalization of Classical Natural Deduction with Disjunction Partially Additive Categories and Fully Complete Models of Linear Logic Distinguishing Data Structures and Functions: The Constructor Calculus and Functorial Types The Finitely Generated Types of the λ-Calculus