Abstract is missing.
- On Mints Reduction for ccc-CalculusYohji Akama. 1-12
- A Formalization of the Strong Normalization Proof for System F in LEGOThorsten Altenkirch. 13-28
- Partial Intersection Type Assignment in Applicative Term Rewriting SystemsSteffen van Bakel. 29-44
- Extracting Constructive Content from Classical Logic via Control-like ReductionsFranco Barbanera, Stefano Berardi. 45-59
- Combining First and Higher Order Rewrite Systems with Type Assignment SystemsFranco Barbanera, Maribel Fernández. 60-74
- A Term Calculus for Intuitionistic Linear LogicP. N. Benton, Gavin M. Bierman, Valeria de Paiva, Martin Hyland. 75-90
- Program Extraction from Normalization ProofsUlrich Berger. 91-106
- A Semantics for Lambda&-early: A Calculus with Overloading and Early BindingGiuseppe Castagna, Giorgio Ghelli, Giuseppe Longo. 107-123
- An Abstract Notion of ApplicationPietro Di Gianantonio, Furio Honsell. 124-138
- The Undecidability of Typability in the Lambda-Pi-CalculusGilles Dowek. 139-145
- Recursive Types Are not Conservative over FGiorgio Ghelli. 146-162
- The Conservation Theorem revisitedPhilippe de Groote. 163-178
- Modified Realizability Toposes and Strong Normalization ProofsJ. M. E. Hyland, C.-H. Luke Ong. 179-194
- Semantics of lambda-I and of other substructure lambda calculiBart Jacobs. 195-208
- Translating Dependent Type Theory into Higher Order LogicBart Jacobs, Thomas F. Melham. 209-229
- Studying the Fully Abstract Model of PCF within its Continuous Function ModelAchim Jung, Allen Stoughton. 230-244
- A New Characterization of Lambda DefinabilityAchim Jung, Jerzy Tiuryn. 245-257
- Combining Recursive and Dynamic TypesHans Leiß. 258-273
- Lambda calculus characterizations of poly-timeDaniel Leivant, Jean-Yves Marion. 274-288
- Pure Type Systems FormalizedJames McKinna, Robert Pollack. 289-305
- Orthogonal Higher-Order Rewrite Systems are ConfluentTobias Nipkow. 306-317
- Monotonic versus Antimonotonic ExponentationDaniel F. Otth. 318-327
- Inductive Definitions in the system Coq - Rules and PropertiesChristine Paulin-Mohring. 328-345
- Intersection Types and Bounded PolymorphismBenjamin C. Pierce. 346-360
- A Logic for Parametric PolymorphismGordon D. Plotkin, Martín Abadi. 361-375
- Call-by-Value and NondeterminismKurt Sieber. 376-390
- Lower and Upper Bounds for Reductions of Types in Lambda-omega and Lambda-PJan Springintveld. 391-405
- Lambda-Calculi with Conditional RulesMasako Takahashi. 406-417
- Type reconstruction in F-omega is undecidablePawel Urzyczyn. 418-432