Abstract is missing.
- Comparing Lambda-calculus translations in Sharing GraphsAndrea Asperti, Cosimo Laneve. 1-15
- Extensions of Pure Type SystemsGilles Barthe. 16-31
- A Model for Formal Parametric Polymorphism: A PER Interpretation for System RRoberto Bellucci, Martín Abadi, Pierre-Louis Curien. 32-46
- A realization of the negative interpretation of the Axiom of ChoiceStefano Berardi, Marc Bezem, Thierry Coquand. 47-62
- Using Subtyping in Program OptimizationStefano Berardi, Luca Boerio. 63-77
- What is a Categorical Model of Intuitionistic Linear Logic?Gavin M. Bierman. 78-93
- An explicit Eta rewrite ruleDaniel Briaud. 94-108
- Extracting Text from ProofsYann Coscoy, Gilles Kahn, Laurent Théry. 109-123
- Higher-Order Abstract Syntax in CoqJoëlle Despeyroux, Amy P. Felty, André Hirschowitz. 124-138
- Expanding Extensional PolymorphismRoberto Di Cosmo, Adolfo Piperno. 139-153
- Lambda-calculus, Combinators and the Comprehension SchemeGilles Dowek. 154-170
- ßn-Equality for CoproductsNeil Ghani. 171-185
- Typed Operational SemanticsHealfdene Goguen. 186-200
- A Simple Calculus of Exception HandlingPhilippe de Groote. 201-215
- A Simple Model for Quotient TypesMartin Hofmann. 216-234
- Untyped lambda-Calculus with Relative TypingM. Randall Holmes. 235-248
- Final Semantics for untyped lambda-calculusFurio Honsell, Marina Lenisa. 249-265
- A Simplification of Girard s ParadoxAntonius J. C. Hurkens. 266-278
- Basic Properties of Data Types with Inequational RefinementsHidetaka Kondoh. 279-296
- Decidable Properties of Intersection Type SystemsToshihiko Kurata, Masako Takahashi. 297-311
- Termination Proof of Term Rewriting System with the Multiset Path Ordering. A Complete Development in the System CoqFrançois Leclerc. 312-327
- Typed lambda-calculi with explicit substitutions may not terminatePaul-André Melliès. 328-334
- On Equivalence Classes of Interpolation EquationsVincent Padovani. 335-349
- Strict Functionals for Termination ProofsJaco van de Pol, Helmut Schwichtenberg. 350-364
- A Verified TypecheckerRobert Pollack. 365-380
- Categorical semantics of the call-by-value lambda-calculusAlberto Pravato, Simona Ronchi Della Rocca, Luca Roversi. 381-396
- A Fully Abstract Translation between a Lambda-Calculus with Reference Types and Standard MLEike Ritter, Andrew M. Pitts. 397-413
- Categorical completeness results for the simply-typed lambda-calculusAlex K. Simpson. 414-427
- Third-Order Matching in the Presence of Type ConstructorsJan Springintveld. 428-442