1.5 Related Reading

< Free Open Study >

While this book attempts to be self contained, it is far from comprehensive; the area is too large, and can be approached from too many angles, to do it justice in one book. This section lists a few other good entry points.

Handbook articles by Cardelli (1996) and Mitchell (1990b) offer quick introductions to the area. Barendregt's article (1992) is for the more mathematically inclined. Mitchell's massive textbook on Foundations for Programming Languages (1996) covers basic lambda-calculus, a range of type systems, and many aspects of semantics. The focus is on semantic rather than implementation issues. Reynolds's Theories of Programming Languages (1998b), a graduate-level survey of the theory of programming languages, includes beautiful expositions of polymorphism, subtyping, and intersection types. The Structure of Typed Programming Languages, by Schmidt (1994), develop score concepts of type systems in the context of language design, including several chapters on conventional imperative languages. Hindley's monograph Basic Simple Type Theory (1997) is a wonderful compendium of results about the simply typed lambda-calculus and closely related systems. Its coverage is deep rather than broad.

Abadi and Cardelli's A Theory of Objects (1996) develops much of the same material as the present book, de-emphasizing implementation aspects and concentrating instead on the application of these ideas in a foundation treatment of object-oriented programming. Kim Bruce's Foundations of Object-Oriented Languages: Types and Semantics (2002) covers similar ground. Introductory material on object-oriented type systems can also be found in Palsberg and Schwartzbach (1994) and Castagna (1997).

Semantic foundations for both untyped and typed languages are covered in depth in the textbooks of Gunter (1992), Winskel (1993), and Mitchell (1996). Operational semantics is also covered in detail by Hennessy (1990). Foundations for the semantics of types in the mathematical framework of category theory can also be found in many sources, including the books by Jacobs(1999), Asperti and Longo (1991), and Crole (1994); a brief primer can be found in Basic Category Theory for Computer Scientists (Pierce, 1991a).

Girard, Lafont, and Taylor's Proofs and Types (1989) treats logical aspects of type systems (the Curry-Howard correspondence, etc.). It also includes a description of System F from its creator, and an appendix introducing linear logic. Connections between types and logic are further explored in Pfenning's Computation and Deduction (2001). Thompson's Type Theory and Functional Programming (1991) and Turner's Constructive Foundations for Functional Languages (1991) focus on connections between functional programming (in the "pure functional programming" sense of Haskell or Miranda) and constructive type theory, viewed from a logical perspective. A number of relevant topics from proof theory are developed in Goubault-Larrecq and Mackie's Proof Theory and Automated Deduction (1997). The history of types in logic and philosophy is described in more detail in articles by Constable (1998), Wadler (2000), Huet (1990), and Pfenning (1999), in Laan's doctoral thesis (1997), and in books by Grattan-Guinness (2001) and Sommaruga (2000).

It turns out that a fair amount of careful analysis is required to avoid false and embarrassing claims of type soundness for programming languages. As a consequence, the classification, description, and study of type systems has emerged as a formal discipline. —Luca Cardelli (1996)

< Free Open Study >