5. TLCA 2001:
: 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.
: Representations of First Order Function Types as Terminal Coalgebras.
: 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.
Philippe de Groote
: Strong Normalization of Classical Natural Deduction with Disjunction.
: Partially Additive Categories and Fully Complete Models of Linear Logic.
C. Barry Jay
: Distinguishing Data Structures and Functions: The Constructor Calculus and Functorial Types.
: The Finitely Generated Types of the lambda-Calculus.
: A Deconstruction of Non-deterministic Classical Cut Elimination.
: Second-Order Pre-Logical Relations and Representation Independence.
: Characterizing Convergent Terms in Object Calculi via Intersection Types.
: Parigot's Second Order lambda-mu-Calculus and Inductive Types.
Jorge Sousa Pinto
: Parallel Implementation Models for the lambda-Calculus Using the Geometry of Interaction.
: Strong Normalisation for a Gentzen-like Cut-Elimination Procedure.