Marc Bezem, Jan Friso Groote
Proceedings of the International Conference on Typed Lambda Calculi and Applications
TLCA, 1993.

@proceedings{TLCA-1993,
	address       = "Utrecht, The Netherlands",
	editor        = "Marc Bezem and Jan Friso Groote",
	isbn          = "3-540-56517-5",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the International Conference on Typed Lambda Calculi and Applications}",
	volume        = 664,
	year          = 1993,
}

Contents (29 items)

4 ×#calculus
4 ×#logic
3 ×#higher-order
3 ×#normalisation
3 ×#proving
3 ×#reduction
3 ×#term rewriting
3 ×#λ-calculus
2 ×#bound
2 ×#morphism

TLCA-1993-Akama #calculus #on the #reduction

On Mints’ Reduction for ccc-Calculus (YA), pp. 1–12.

TLCA-1993-Altenkirch #formal method #normalisation #proving #system f

A Formalization of the Strong Normalization Proof for System F in LEGO (TA), pp. 13–28.

TLCA-1993-Bakel #term rewriting

Partial Intersection Type Assignment in Applicative Term Rewriting Systems (SvB), pp. 29–44.

TLCA-1993-BarbaneraB #logic #reduction

Extracting Constructive Content from Classical Logic via Control-like Reductions (FB, SB), pp. 45–59.

TLCA-1993-BarbaneraF #higher-order #term rewriting

Combining First and Higher Order Rewrite Systems with Type Assignment Systems (FB, MF), pp. 60–74.

TLCA-1993-BentonBPH #calculus #linear #logic

A Term Calculus for Intuitionistic Linear Logic (PNB, GMB, VdP, MH), pp. 75–90.

TLCA-1993-Berger #normalisation #proving

Program Extraction from Normalization Proofs (UB0), pp. 91–106.

TLCA-1993-CastagnaGL #calculus #semantics

A Semantics for λ&-early: A Calculus with Overloading and Early Binding (GC, GG, GL), pp. 107–123.

TLCA-1993-GianantonioH

An Abstract Notion of Application (PDG, FH), pp. 124–138.

TLCA-1993-Dowek #calculus

The Undecidability of Typability in the λ-π-Calculus (GD), pp. 139–145.

TLCA-1993-Ghelli #recursion

Recursive Types Are not Conservative over F (GG), pp. 146–162.

TLCA-1993-Groote #revisited #theorem

The Conservation Theorem revisited (PdG), pp. 163–178.

TLCA-1993-HylandO #normalisation #proving

Modified Realizability Toposes and Strong Normalization Proofs (JMEH, CHLO), pp. 179–194.

TLCA-1993-Jacobs #semantics #λ-calculus

Semantics of λ-I and of other substructure λ calculi (BJ0), pp. 195–208.

TLCA-1993-JacobsM #dependent type #higher-order #logic #type system

Translating Dependent Type Theory into Higher Order Logic (BJ, TFM), pp. 209–229.

TLCA-1993-JungS

Studying the Fully Abstract Model of PCF within its Continuous Function Model (AJ, AS), pp. 230–244.

TLCA-1993-JungT

A New Characterization of λ Definability (AJ, JT), pp. 245–257.

TLCA-1993-Leiss #recursion

Combining Recursive and Dynamic Types (HL), pp. 258–273.

TLCA-1993-LeivantM #λ-calculus

λ calculus characterizations of poly-time (DL, JYM), pp. 274–288.

TLCA-1993-McKinnaP #type system

Pure Type Systems Formalized (JM, RP), pp. 289–305.

TLCA-1993-Nipkow #confluence #higher-order #orthogonal #term rewriting

Orthogonal Higher-Order Rewrite Systems are Confluent (TN), pp. 306–317.

TLCA-1993-Otth

Monotonic versus Antimonotonic Exponentation (DFO), pp. 318–327.

TLCA-1993-Paulin-Mohring #coq #induction

Inductive Definitions in the system Coq — Rules and Properties (CPM), pp. 328–345.

TLCA-1993-Pierce #bound #morphism #polymorphism

Intersection Types and Bounded Polymorphism (BCP), pp. 346–360.

TLCA-1993-PlotkinA #logic #morphism #parametricity #polymorphism

A Logic for Parametric Polymorphism (GDP, MA), pp. 361–375.

TLCA-1993-Sieber #call-by #nondeterminism

Call-by-Value and Nondeterminism (KS), pp. 376–390.

TLCA-1993-Springintveld #bound #reduction

Lower and Upper Bounds for Reductions of Types in λω and λP (JS), pp. 391–405.

TLCA-1993-Takahashi #λ-calculus

λ-Calculi with Conditional Rules (MT), pp. 406–417.

TLCA-1993-Urzyczyn #decidability #re-engineering

Type reconstruction in Fω is undecidable (PU), pp. 418–432.