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)

6 ×#λ-calculus
4 ×#calculus
4 ×#type system
3 ×#game studies
3 ×#higher-order
3 ×#logic
3 ×#normalisation
2 ×#algebra
2 ×#category theory
2 ×#complexity

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.