Types and Programming Languages

Pierce, B. C. (2002). Types and Programming Languages. MIT Press.

Type

Book

Intellectual base

Review or monograph

Year

2002

Link

https://mitpress.mit.edu/9780262162098/types-and-programming-languages/

Cited from

computer_science, mathematics, philosophy, systems_cybernetics

Cited by

13 citations across 12 artifacts.

Each citation links to the sentence it supports in the citing article.

Primes

• Asymmetric Interface Tolerance
  • The argument for static typing is structurally the same as the argument for strict schema validation — catch drift early, accept short-term friction for long-term clarity.

    This sourceFoundational text on static type systems as a strict-receiver discipline that catches errors early at the cost of short-term friction — structurally the case for strict schema validation.

• Closure
  • Type-system design enforces closure of the type-formation rules: from base types one constructs sums, products, function types, and higher-kinded types via closure under designated type formers, and the soundness theorem of a type system is essentially the assertion that the typing judgment is closed under reduction (a well-typed term reduces to a well-typed term — subject reduction) and under value-formation (a well-typed value is in the value class of its type — progress), as Pierce (2002) develops as the canonical organisational scheme of type-system soundness proofs.

    This sourceCanonical graduate type-theory text developing soundness via preservation (subject reduction) and progress — the two closure properties whose conjunction implies well-typed programs do not get stuck.

• Consistency
  • A growing company's vacation policy that simultaneously requires unlimited rollover, caps balances at a fixed maximum, and credits more days than some employees use is jointly unsatisfiable for the light users, and the HR task — find the minimal conflicting subset, then add a scope qualifier such as a capped-rollover-with-payout rule rather than rewriting the policy — is structurally the same operation a compiler performs on conflicting type constraints

    This sourceStandard reference on type systems; treats conflicting type constraints and the checker's role in rejecting inconsistent constraint sets.

• Deductive Reasoning

  • This sourceBibliography-only; type systems presented as deductive systems.

  • A software engineer uses a type system (e.g., Hindley-Milner in languages like Haskell, or dependent types in languages like Coq, Agda, or Lean

    This sourceStandard text presenting type systems as deductive systems (typing rules in natural-deduction style, type inference, the propositions-as-types / Curry–Howard correspondence); the type checker is a proof engine. WebSearch confirmed the natural-deduction-style typing rules and Curry–Howard theme.

• Disjointness
  • In type systems, sum types treat cases as disjoint, which is exactly what makes pattern matching exhaustive.

    This sourceStandard type-theory text in which sum (variant) types model mutually exclusive disjoint cases, which is precisely what makes pattern matching over them exhaustive.

• Self Checking
  • In software engineering it is assertions, invariants, runtime contracts, property-based tests, and type checking, where the type derivation is a redundant path against the value computation.

    This sourceEstablishes type checking as a redundant derivation about a program's values that flags inconsistency, the basis for treating a type derivation as a self-checking path.

• Union
  • In type theory and programming it is the sum type (variant, tagged union, Either, discriminated union): a value of type A | B is a value that is an A or a B, the type-level union of the two value sets, dual to the product/record type that pairs them.

    This sourceDefines sum (variant/tagged-union) types as the type-level union of value sets — a value of type A | B being an A or a B — dual to product types.

Domain-specific

• Subject reduction
  • The entry records a descriptive analytical identity; practical use requires the governing domain's evidence, standards, and safety obligations.
• Type constructor
  • … transfers from Applying the unary list constructor to integer produces the type list of integer, while the binary function constructor maps input and output types to a function type. to A compiler separates a constructor from a fully applied type and enforces higher-kinded arity where partial application is allowed..
• Type System
  • The load-bearing guarantee is type soundness, expressed by Milner's slogan "well-typed programs cannot go wrong": a typing judgment (in the static case, a formal proof derivable by the language's type rules) certifies that a program will not reach a state of applying an operation to an argument of the wrong kind — no integer treated as a function pointer, no null pointer dereferenced as a record, no float passed where a string is expected — and two meta-theorems, progress and preservation, formalize this guarantee as a structural induction over the operational semantics

    This sourceEstablishes type soundness as the conjunction of the progress and preservation theorems, proved by induction on typing derivations; the 'well-typed programs cannot go wrong' slogan is Milner's (1978).

• Typing rule
  • A typing rule is an inference schema defining when a term has a type under a context.
• Unit type
  • The entry records a descriptive analytical identity; practical use requires the governing domain's evidence, standards, and safety obligations.

Verification

This reference passed the adversarial substantiation pipeline: it was checked to exist and to support the claim it is attached to. See how references were verified.

Links previously used in the corpus

Before the registry existed this work was also linked 1 other way.

• https://www.cis.upenn.edu/~bcpierce/tapl/ ×1

Registry ID ref:bf38292b73c2 · see in the full table