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