Table of Contents

Comparing—-calculus translations in sharing graphs.- Extensions of pure type systems.- A model for formal parametric polymorphism: A per interpretation for system R.- A realization of the negative interpretation of the Axiom of Choice.- Using subtyping in program optimization.- What is a categorical model of Intuitionistic Linear Logic?.- An explicit Eta rewrite rule.- Extracting text from proofs.- Higher-order abstract syntax in Coq.- Expanding extensional polymorphism.- Lambda-calculus, combinators and the comprehension scheme.-—?-Equality for coproducts.- Typed operational semantics.- A simple calculus of exception handling.- A simple model for quotient types.- Untyped—-calculus with relative typing.- Final semantics for untyped—-calculus.- A simplification of Girard's paradox.- Basic properties of data types with inequational refinements.- Decidable properties of intersection type systems.- Termination proof of term rewriting system with the multiset path ordering. A complete development in the system Coq.- Typed—-calculi with explicit substitutions may not terminate.- On equivalence classes of interpolation equations.- Strict functionals for termination proofs.- A verified typechecker.- Categorical semantics of the call-by-value—-calculus.- A fully abstract translation between a—-calculus with reference types and Standard ML.- Categorical completeness results for the simply-typed lambda-calculus.- Third-order matching in the presence of type constructors.