## 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)

- 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.

4 ×#calculus

4 ×#logic

3 ×#higher-order

3 ×#normalisation

3 ×#proving

3 ×#reduction

3 ×#term rewriting

3 ×#λ-calculus

2 ×#bound

2 ×#morphism

4 ×#logic

3 ×#higher-order

3 ×#normalisation

3 ×#proving

3 ×#reduction

3 ×#term rewriting

3 ×#λ-calculus

2 ×#bound

2 ×#morphism