Back to Papers

Types and Programming Languages

Authors

Benjamin C. Pierce

Year

2002

Abstract

A comprehensive introduction to type systems and programming language theory.

BibTeX

            @book{pierce2002types, title={Types and Programming Languages}, author={Pierce, Benjamin C.}, year={2002}, publisher={MIT Press}}

Notations Used in This Paper

for Lambda Abstraction

A function definition in lambda calculus

Typst: $lambda x. e$
LaTeX: \lambda x. e

Context: Used throughout the book

Referenced on page 15

for Type Judgment

A formal statement asserting that a term has a certain type in a given context

Typst: $Gamma tack.r e : tau$
LaTeX: \Gamma \vdash e : \tau

Context: Introduced in Chapter 3 as the fundamental judgment of type systems

Referenced on page 32

Primary Definition