The Structure of Typed Programming Languages

The Structure of Typed Programming Languages describes the fundamental
syntactic and semantic features of modern programming languages, carefully spelling
out their impacts on language design. Using classical and recent research from
lambda calculus and type theory, it presents a rational reconstruction of the
Algol-like imperative languages such as Pascal, Ada, and Modula-3, and the
higher-order functional languages such as Scheme and ML.David Schmidt's text is
based on the premise that although few programmers ever actually design a
programming language, it is important for them to understand the structuring
techniques. His use of these techniques in a reconstruction of existing programming
languages and in the design of new ones allows programmers and would-be programmers
to see why existing languages are structured the way they are and how new languages
can be built using variations on standard themes.The text is unique in its tutorial
presentation of higher-order lambda calculus and intuitionistic type theory. The
latter in particular reveals that a programming language is a logic in which its
typing system defines the propositions of the logic and its well-typed programs
constitute the proofs of the propositions.The Structure of Typed Programming
Languages is designed for use in a first or second course on principles of
programming languages. It assumes a basic knowledge of programming languages and
mathematics equivalent to a course based on books such as Friedman, Wand, and
Haynes': Essentials of Programming Languages. As Schmidt covers both the syntax and
the semantics of programming languages, his text provides a perfect precursor to a
more formal presentation of programming language semantics such as Gunter's
Semantics of Programming Languages.