Logical Foundations of Functional Programming

 Content: CAML : the theory, the machine, and the language : introduction / Guy Cousineau --
 Cartesian closed categories and lambda-calculus / Gerard Huet --
 The categorical abstract machine / Guy Cousineau --
 Compiling ML into CAM / Ascander Suarez --
 Polymorphic lambda-calculus : introduction / John C. Reynolds --
 The system F of variable types, 15 years later / Jean-Yves Girard --
 On functors expressible in the polymorphic lambda calculus / John C. Reynolds and Gordon D. Plotkin --
 Polymorphic type inference and containment / John C. Mitchell --
 A type-inference approach to reduction properties and semantics of polymorphic expressions (summary) / John C. Mitchell. The semantics of second-order lambda-calculus / Kim B. Bruce, Albert R. Meyer, and John C. Mitchell --
 Empty types in polymorphic lambda-calculus / Albert R. Meyer [and others] --
 Computable values can be classical / Val Breazu-Tannen and Albert R. Meyer / Polymorphism is conservative over simple types / Val Breazu-Tannen and Albert R. Meyer --
 Functorial polymorphism / E.S. Bainbridge [and others] --
 Topics in constructive type theory : introduction / Gerard Huet --
 A uniform approach to type theory / Gerard Huet --
 On the analogy between propositions and types / Thierry Coquand --
 Recursive realizability semantics for calculus of constructions / Andre Scedrov --
 An introduction to PX / Susumu Hayashi.