Philippe de Groote
Proceedings of the Fourth International Conference on Typed Lambda Calculi and Applications
TLCA, 1997.

@proceedings{TLCA-1997,
	address       = "Nancy, France",
	editor        = "Philippe de Groote",
	isbn          = "3-540-62688-3",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Fourth International Conference on Typed Lambda Calculi and Applications}",
	volume        = 1210,
	year          = 1997,
}

Contents (24 items)

5 ×#λ-calculus
3 ×#calculus
3 ×#recursion
3 ×#type system
2 ×#axiom
2 ×#category theory
2 ×#induction
2 ×#logic
2 ×#normalisation
2 ×#proving

TLCA-1997-Akama #normalisation

A λ-to-CL Translation for Strong Normalization (YA), pp. 1–10.

TLCA-1997-BelleM #analysis

Typed Intermediate Languages for Shape Analysis (GB, EM), pp. 11–29.

TLCA-1997-BerardiB #data type #functional

Minimum Information Code in a Pure Functional Language with Data Types (SB, LB), pp. 30–45.

TLCA-1997-BonoB #constraints #λ-calculus

Matching Constraints for the λ Calculus of Objects (VB, MB), pp. 46–62.

TLCA-1997-BrandtH #axiom #induction #recursion #similarity #type system

Coinductive Axiomatization of Recursive Type Equality and Subtyping (MB, FH), pp. 63–81.

TLCA-1997-Brauner #category theory

A Simple Adequate Categorical Model for PCF (TB), pp. 82–98.

TLCA-1997-Buciarelli #logic #re-engineering

Logical Reconstruction of Bi-domains (AB), pp. 99–111.

TLCA-1997-Courant #calculus #type system

A Module Calculus for Pure Type Systems (JC), pp. 112–128.

TLCA-1997-DamianiG #algorithm #strict

An Inference Algorithm for Strictness (FD, PG), pp. 129–146.

TLCA-1997-DespeyrouxPS #higher-order #recursion #syntax

Primitive Recursion for Higher-Order Abstract Syntax (JD, FP, CS), pp. 147–163.

TLCA-1997-Ghani #calculus #dependent type #type system

Eta-Expansions in Dependent Type Theory — The Calculus of Constructions (NG), pp. 164–180.

TLCA-1997-GuerriniMM #proving

Proof Nets, Garbage, and Computations (SG, SM, AM), pp. 181–195.

TLCA-1997-Hasegawa #category theory #modelling #recursion #λ-calculus

Recursion from Cyclic Sharing: Traced Monoidal Categories and Models of Cyclic λ Calculi (MH), pp. 196–213.

TLCA-1997-Herbelin #game studies #reduction

Games and Weak-Head Reduction for Classical PCF (HH), pp. 214–230.

TLCA-1997-Kurata

A Type Theoretical View of Böhm-Trees (TK), pp. 231–247.

TLCA-1997-Lenisa #induction #semantics #λ-calculus

Semantic Techniques for Deriving Coinductive Characterizations of Observational Equivalences for λ-calculi (ML), pp. 248–266.

TLCA-1997-MalolepszyMZ #decidability

Schwichtenberg-Style λ Definability Is Undecidable (JM, MM, MZ), pp. 267–283.

TLCA-1997-Raamsdonk

Outermost-Fair Rewriting (FvR), pp. 284–299.

TLCA-1997-RetoreL #commutative #linear #logic

A Non-commutative Extension of Classical Linear Logic (CR, PL), pp. 300–318.

TLCA-1997-Ruess #calculus #proving #theorem proving

Computational Reflection in the Calculus of Constructions and its Application to Theorem Proving (HR), pp. 319–335.

TLCA-1997-Stark #equation

Names, Equations, Relations: Practical Ways to Reason about new (IS), pp. 336–353.

TLCA-1997-Takeuti #axiom #parametricity

An Axiomatic System of Parametricity (IT), pp. 354–372.

TLCA-1997-Urzyczyn #approach #λ-calculus

Inhabitation in Typed λ-Calculi (A Syntactic Approach) (PU), pp. 373–389.

TLCA-1997-Xi #normalisation #λ-calculus

Weak and Strong β Normalisations in Typed λ-Calculi (HX), pp. 390–404.