Mariangiola Dezani-Ciancaglini, Gordon D. Plotkin
Proceedings of the Second International Conference on Typed Lambda Calculi and Applications
TLCA, 1995.

@proceedings{TLCA-1995,
	address       = "Edinburgh, Scotland, United Kingdom",
	editor        = "Mariangiola Dezani-Ciancaglini and Gordon D. Plotkin",
	isbn          = "3-540-59048-X",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Second International Conference on Typed Lambda Calculi and Applications}",
	volume        = 902,
	year          = 1995,
}

Contents (29 items)

8 ×#λ-calculus
4 ×#type system
3 ×#category theory
3 ×#proving
3 ×#semantics
2 ×#coq
2 ×#equation
2 ×#higher-order
2 ×#morphism
2 ×#polymorphism

TLCA-1995-AspertiL #graph #λ-calculus

Comparing λ-calculus translations in Sharing Graphs (AA, CL), pp. 1–15.

TLCA-1995-Barthe #type system

Extensions of Pure Type Systems (GB), pp. 16–31.

TLCA-1995-BellucciAC #morphism #parametricity #polymorphism

A Model for Formal Parametric Polymorphism: A PER Interpretation for System R (RB, MA, PLC), pp. 32–46.

TLCA-1995-BerardiBC #axiom

A realization of the negative interpretation of the Axiom of Choice (SB, MB, TC), pp. 47–62.

TLCA-1995-BerardiB #optimisation #type system #using

Using Subtyping in Program Optimization (SB, LB), pp. 63–77.

TLCA-1995-Bierman #category theory #linear #logic #question #what

What is a Categorical Model of Intuitionistic Linear Logic? (GMB), pp. 78–93.

TLCA-1995-Briaud

An explicit Eta rewrite rule (DB), pp. 94–108.

TLCA-1995-CoscoyKT #proving

Extracting Text from Proofs (YC, GK, LT), pp. 109–123.

TLCA-1995-DespeyrouxFH #coq #higher-order #syntax

Higher-Order Abstract Syntax in Coq (JD, APF, AH), pp. 124–138.

TLCA-1995-CosmoP #morphism #polymorphism

Expanding Extensional Polymorphism (RDC, AP), pp. 139–153.

TLCA-1995-Dowek #combinator #comprehension #λ-calculus

λ-calculus, Combinators and the Comprehension Scheme (GD), pp. 154–170.

TLCA-1995-Ghani

ßn-Equality for Coproducts (NG), pp. 171–185.

TLCA-1995-Goguen #semantics

Typed Operational Semantics (HG), pp. 186–200.

TLCA-1995-Groote #calculus #exception

A Simple Calculus of Exception Handling (PdG), pp. 201–215.

TLCA-1995-Hofmann

A Simple Model for Quotient Types (MH0), pp. 216–234.

TLCA-1995-Holmes #type system #λ-calculus

Untyped λ-Calculus with Relative Typing (MRH), pp. 235–248.

TLCA-1995-HonsellL #semantics #λ-calculus

Final Semantics for untyped λ-calculus (FH, ML), pp. 249–265.

TLCA-1995-Hurkens

A Simplification of Girard’s Paradox (AJCH), pp. 266–278.

TLCA-1995-Kondoh #data type #equation

Basic Properties of Data Types with Inequational Refinements (HK), pp. 279–296.

TLCA-1995-KurataT #decidability #type system

Decidable Properties of Intersection Type Systems (TK, MT), pp. 297–311.

TLCA-1995-Leclerc #coq #development #multi #order #proving #term rewriting #termination

Termination Proof of Term Rewriting System with the Multiset Path Ordering. A Complete Development in the System Coq (FL), pp. 312–327.

TLCA-1995-Mellie #λ-calculus

Typed λ-calculi with explicit substitutions may not terminate (PAM), pp. 328–334.

TLCA-1995-Padovani #equation #equivalence #on the

On Equivalence Classes of Interpolation Equations (VP), pp. 335–349.

TLCA-1995-PolS #proving #strict #termination

Strict Functionals for Termination Proofs (JvdP, HS), pp. 350–364.

TLCA-1995-Pollack

A Verified Typechecker (RP), pp. 365–380.

TLCA-1995-PravatoRR #call-by #category theory #semantics #λ-calculus

Categorical semantics of the call-by-value λ-calculus (AP, SRDR, LR), pp. 381–396.

TLCA-1995-RitterP #ml #standard #λ-calculus

A Fully Abstract Translation between a λ-Calculus with Reference Types and Standard ML (ER, AMP), pp. 397–413.

TLCA-1995-Simpson #category theory #λ-calculus

Categorical completeness results for the simply-typed λ-calculus (AKS), pp. 414–427.

TLCA-1995-Springintveld #higher-order

Third-Order Matching in the Presence of Type Constructors (JS), pp. 428–442.