## Samson Abramsky

*Proceedings of the Fifth International Conference on Typed Lambda Calculi and Applications*

TLCA, 2001.

@proceedings{TLCA-2001, address = "Krakow, Poland", editor = "Samson Abramsky", isbn = "3-540-41960-8", publisher = "{Springer-Verlag}", series = "{Lecture Notes in Computer Science}", title = "{Proceedings of the Fifth International Conference on Typed Lambda Calculi and Applications}", volume = 2044, year = 2001, }

### Contents (32 items)

- TLCA-2001-Danvy
- Many Happy Returns (OD), p. 1.
- TLCA-2001-Hofmann #behaviour #bound #complexity #memory management #type system #using
- From Bounded Arithmetic to Memory Management: Use of Type Theory to Capture Complexity Classes and Space Behaviour (MH0), pp. 2–3.
- TLCA-2001-Normann #calculus
- Definability of Total Objects in PCF and Related Calculi (DN), pp. 4–5.
- TLCA-2001-Selinger #category theory #semantics
- Categorical Semantics of Control (PS), pp. 6–7.
- TLCA-2001-Altenkirch #algebra #first-order
- Representations of First Order Function Types as Terminal Coalgebras (TA), pp. 8–21.
- TLCA-2001-AltenkirchC #polymorphism #λ-calculus
- A Finitary Subsystem of the Polymorphic λ-Calculus (TA, TC), pp. 22–28.
- TLCA-2001-BergerHY #π-calculus
- Sequentiality and the π-Calculus (MB, KH, NY), pp. 29–45.
- TLCA-2001-CardelliG #logic #strict
- Logical Properties of Name Restriction (LC, ADG), pp. 46–60.
- TLCA-2001-Chroboczek #game studies #recursion #type system
- Subtyping Recursive Games (JC), pp. 61–75.
- TLCA-2001-CoppolaM #constraints #linear #logic #type system
- Typing λ Terms in Elementary Logic with Linear Constraints (PC, SM), pp. 76–90.
- TLCA-2001-Danner #dependent type
- Ramified Recurrence with Dependent Types (ND), pp. 91–105.
- TLCA-2001-Gianantonio #game studies #lazy evaluation #semantics #λ-calculus
- Game Semantics for the Pure Lazy λ-calculus (PDG), pp. 106–120.
- TLCA-2001-DoughertyL #reduction
- Reductions, Intersection Types, and Explicit Substitutions (DJD, PL), pp. 121–135.
- TLCA-2001-Dowek #modulo theories
- The Stratified Foundations as a Theory Modulo (GD), pp. 136–150.
- TLCA-2001-Filinski #evaluation #normalisation #λ-calculus
- Normalization by Evaluation for the Computational λ-Calculus (AF), pp. 151–165.
- TLCA-2001-Geuvers #dependent type #higher-order #induction #type system
- Induction Is Not Derivable in Second Order Dependent Type Theory (HG), pp. 166–181.
- TLCA-2001-Groote #deduction #normalisation
- Strong Normalization of Classical Natural Deduction with Disjunction (PdG), pp. 182–196.
- TLCA-2001-Haghverdi #category theory #linear #logic #modelling
- Partially Additive Categories and Fully Complete Models of Linear Logic (EH), pp. 197–216.
- TLCA-2001-Jay #calculus #data type
- Distinguishing Data Structures and Functions: The Constructor Calculus and Functorial Types (CBJ), pp. 217–239.
- TLCA-2001-Joly #λ-calculus
- The Finitely Generated Types of the λ-Calculus (TJ), pp. 240–252.
- TLCA-2001-KnapikNU #algebra #monad
- Deciding Monadic Theories of Hyperalgebraic Trees (TK, DN, PU), pp. 253–267.
- TLCA-2001-Laird #nondeterminism
- A Deconstruction of Non-deterministic Classical Cut Elimination (JL), pp. 268–282.
- TLCA-2001-Laurent #geometry #interactive
- A Token Machine for Full Geometry of Interaction (OL), pp. 283–297.
- TLCA-2001-Leiss #higher-order #independence #representation
- Second-Order Pre-Logical Relations and Representation Independence (HL), pp. 298–314.
- TLCA-2001-deLiguoro #calculus #convergence
- Characterizing Convergent Terms in Object Calculi via Intersection Types (Ud), pp. 315–328.
- TLCA-2001-Matthes #higher-order #induction #λ-calculus #μ-calculus
- Parigot’s Second Order λμ-Calculus and Inductive Types (RM), pp. 329–343.
- TLCA-2001-Miquel #calculus
- The Implicit Calculus of Constructions (AM), pp. 344–359.
- TLCA-2001-MurawskiO #evolution #game studies #morphism #polymorphism
- Evolving Games and Essential Nets for Affine Polymorphism (ASM, CHLO), pp. 360–375.
- TLCA-2001-Padovani
- Retracts in Simple Types (VP), pp. 376–384.
- TLCA-2001-Pinto #geometry #implementation #interactive #modelling #parallel #using #λ-calculus
- Parallel Implementation Models for the λ-Calculus Using the Geometry of Interaction (JSP), pp. 385–399.
- TLCA-2001-Schubert #complexity #order
- The Complexity of β-Reduction in Low Orders (AS), pp. 400–414.
- TLCA-2001-Urban #normalisation
- Strong Normalisation for a Gentzen-like Cut-Elimination Procedure (CU), pp. 415–430.

6 ×#λ-calculus

4 ×#calculus

4 ×#type system

3 ×#game studies

3 ×#higher-order

3 ×#logic

3 ×#normalisation

2 ×#algebra

2 ×#category theory

2 ×#complexity

4 ×#calculus

4 ×#type system

3 ×#game studies

3 ×#higher-order

3 ×#logic

3 ×#normalisation

2 ×#algebra

2 ×#category theory

2 ×#complexity