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