Programming languages, from type systems and semantics to what ownership buys you

Why this subject matters now

For most of the field's history, type theory lived in two rooms that rarely spoke. In one, functional-language designers used the Hindley-Milner discipline to make programs that a compiler could type without a single written annotation, and proved metatheorems about soundness and parametricity. In the other, systems programmers wrote C, accepted that memory safety was their personal responsibility, and paid for the mistakes in the security columns of every threat report ever published. The last decade collapsed the wall between those rooms. Rust took an idea that had been an academic curiosity since Girard and Wadler, the linear or affine type that constrains how many times a value may be used, and turned it into a production systems language whose type checker statically rules out use-after-free, double-free, and data races without a garbage collector. RustBelt then supplied the missing proof that the unsafe core those guarantees rest on is actually sound. That is why a systems engineer in 2026 is expected to know what "moved value" means in terms of affine logic, not just as a compiler error.

At the same time the dynamic-language world rediscovered types from the other side. TypeScript put a structural, gradually-typed layer over JavaScript and became one of the most used languages on Earth. Python grew a gradual type system through PEP 484 and the tools that check it. Gradual typing, formalized by Siek and Taha and given its soundness account by Wadler and Findler under the slogan "well-typed programs can't be blamed", is now the daily experience of millions of programmers who have never heard the phrase. A practitioner today is expected to reason about the boundary between checked and unchecked code, to know why a cast can fail at runtime and whose fault it is when it does, and to understand the performance tax that boundary imposes. The material below is the common foundation under all of it, an operational semantics to say what a program does, a type system to constrain what it can do, and a soundness proof to guarantee the second statement actually governs the first.

How operational semantics gives a program meaning

Before a type can be sound, "sound with respect to what?" must have an answer. An operational semantics answers it by defining a relation of computation directly on the syntax of terms, with no appeal to a compiler or a machine. Winskel's textbook and Harper's build the whole edifice this way, and it is the style every modern soundness proof uses. Take a minimal language of arithmetic and booleans, deliberately tiny so that every rule fits on one line.

The values are the finished results, the booleans \(\texttt{true},\texttt{false}\) and the numeric values \(\texttt{0}, \texttt{succ 0}, \texttt{succ(succ 0)}, \dots\). A small-step semantics defines a relation \(t \to t'\), "t reduces to t' in one step", by inference rules. Each rule says that if everything above the line holds, the thing below the line holds. Rules with nothing above the line are axioms.

The two computation rules, E-IfTrue and E-IfFalse, do real work. E-If is a congruence rule that says "keep reducing the guard until it is a value". This split is the whole design. The congruence rules impose an evaluation order, and the computation rules define what a redex means. In E-PredSucc, \(nv\) ranges only over numeric values, which is what makes the rule deterministic and keeps \(\texttt{pred (succ (pred 0))}\) from taking a wrong turn.

A big-step semantics instead defines \(t \Downarrow v\), "t evaluates to the final value v", collapsing the whole computation into one judgment. The if-rule becomes

The two styles agree on terminating programs, in the sense that \(t \Downarrow v\) if and only if \(t \to^{*} v\) with \(v\) a value, where \(\to^{*}\) is the reflexive-transitive closure of \(\to\). They disagree on non-terminating ones, and that disagreement is why soundness proofs prefer small-step. A big-step semantics simply produces no derivation for a divergent program, so it cannot distinguish a program that loops forever (acceptable) from one that gets stuck at a nonsensical state like \(\texttt{succ true}\) (a type error we want to forbid). The small-step relation exposes stuck states as terms that are not values and yet have no \(t'\) with \(t \to t'\). Type soundness, in this framing, is precisely the statement that a well-typed term is never stuck.

A reduction sequence by hand

Reduce \(\texttt{if iszero (pred (succ 0)) then 0 else succ 0}\) under the small-step rules. Write \(g\) for the guard \(\texttt{iszero (pred (succ 0))}\). Evaluation is left-to-right and innermost-guard-first because of the congruence rules.

  if iszero (pred (succ 0)) then 0 else succ 0
     |  E-If needs the guard reduced; guard is iszero(...),
     |  and E-IsZero's congruence needs its argument reduced;
     |  that argument is pred(succ 0), a redex for E-PredSucc.
     v   E-PredSucc:  pred (succ 0)  ->  0
  if iszero 0 then 0 else succ 0
     |  E-IszeroZero:  iszero 0  ->  true
     v
  if true then 0 else succ 0
     |  E-IfTrue
     v
  0                                   (a value; no rule applies; done)

Three steps, ending in the numeric value \(\texttt{0}\). Every intermediate term is well-formed and every step was forced. At each point exactly one rule applied, which is the content of the determinism lemma (if \(t \to t'\) and \(t \to t''\) then \(t' = t''\)), proved by a routine induction on the derivation of the first step. Determinism is not required for soundness but it is what lets us speak of "the" result.

The lambda calculus

Arithmetic terms cannot express abstraction, and abstraction is the whole subject. Church's lambda calculus adds exactly three forms, and it is Turing-complete with only these.

A variable, a function \(\lambda x.\,t\) that binds \(x\) in body \(t\), and an application \(t_1\,t_2\). The one computation rule is beta reduction. Applying a function substitutes the argument for the bound variable.

Substitution \([x := s]\,t\) must be capture-avoiding, meaning free variables of \(s\) must not be accidentally bound by a \(\lambda\) inside \(t\). The standard hazard is \((\lambda x.\, \lambda y.\, x)\, y\). A naive textual replacement gives \(\lambda y.\, y\), the identity, when the intended result is a constant function returning the outer \(y\). The fix is to rename the bound \(y\) first (alpha-conversion, \(\lambda y.\,x \equiv \lambda z.\,x\)), giving \(\lambda z.\, y\). Terms are always identified up to alpha, so \(\lambda x.\,x\) and \(\lambda w.\,w\) are literally the same term.

Church encodings

Data is unnecessary as a primitive, since it can be encoded as behavior. A Church numeral represents \(n\) as "apply a function \(n\) times".

Successor is \(\textsf{succ} = \lambda n.\lambda s.\lambda z.\, s\,(n\,s\,z)\), and the booleans are the two projections \(\textsf{tru} = \lambda t.\lambda f.\,t\) and \(\textsf{fls} = \lambda t.\lambda f.\,f\), so that \(\textsf{if}\,b\,x\,y\) is just \(b\,x\,y\). These encodings matter here for one reason. They show that even an untyped calculus with three constructors has enough structure to make typing interesting, and, as the next section shows, that the simplest type discipline is already strong enough to reject some of them (the fixed-point combinator, hence general recursion, does not type in the simply-typed calculus).

Confluence and Church-Rosser

The calculus is nondeterministic, since a term can have several redexes. \((\lambda x.\,x\,x)\,((\lambda y.\,y)\,z)\) can reduce the outer application first or the inner one. The Church-Rosser theorem says the choice does not matter for the final answer.

Theorem (Church-Rosser). If \(t \to_\beta^{*} t_1\) and \(t \to_\beta^{*} t_2\), then there exists \(t_3\) with \(t_1 \to_\beta^{*} t_3\) and \(t_2 \to_\beta^{*} t_3\). The relation \(\to_\beta^{*}\) is confluent.

The proof is out of scope. The clean modern argument is the Tait-Martin-Löf technique of a parallel reduction relation that satisfies the diamond property in one step, whose transitive closure is exactly \(\to_\beta^{*}\). It is written out in full in Barendregt's monograph and in Pierce, chapter on the untyped calculus. Two corollaries are what we use. First, normal forms are unique. A term has at most one irreducible form, so "the value of a program" is well defined independent of evaluation order. Second, evaluation order affects only termination, not the answer, which is why a lazy language and a strict language that both terminate compute the same result.

The simply-typed lambda calculus and type soundness

This is the centerpiece. Add the smallest interesting type structure to the lambda calculus, then prove that well-typed programs do not go wrong. The proof technique, progress plus preservation, is due to Wright and Felleisen (1994) and is now the default. It is worth doing in full because every richer soundness proof, up to RustBelt, is this same skeleton with more cases.

Syntax, values, and the reduction relation

Terms, types, and values for the language \(\lambda^{\to}\) with booleans.

Call-by-value small-step reduction. The two computation rules are beta (E-AppAbs) and the two if-rules. The rest are congruences fixing left-to-right, argument-after-function order.

The typing judgment is \(\Gamma \vdash t : T\), read "under context \(\Gamma\), term \(t\) has type \(T\)", where \(\Gamma\) is a finite map from variables to types. There are six rules.

The claim to prove is type soundness. If \(\varnothing \vdash t : T\) then evaluation of \(t\) never gets stuck. It decomposes into two theorems.

Progress

Theorem (Progress). If \(\varnothing \vdash t : T\) (t is closed and well-typed), then either \(t\) is a value or there exists \(t'\) with \(t \to t'\).

The proof needs a lemma classifying the values of each type, which is where the shape of the constructors is pinned down.

Canonical Forms Lemma. (1) If \(v\) is a value with \(\varnothing \vdash v : \texttt{Bool}\) then \(v\) is \(\texttt{true}\) or \(\texttt{false}\). (2) If \(v\) is a value with \(\varnothing \vdash v : T_1 \to T_2\) then \(v = \lambda x{:}T_1.\,t\) for some body \(t\). Proof. By the grammar, a value is \(\texttt{true},\texttt{false}\), or an abstraction. Inspect each against the type. An abstraction is typed only by T-Abs, whose conclusion is an arrow, so it cannot have type \(\texttt{Bool}\). \(\texttt{true}\) and \(\texttt{false}\) are typed only by T-True, T-False, whose conclusion is \(\texttt{Bool}\), so neither has an arrow type. The two clauses follow by elimination. \(\blacksquare\)

Proof of Progress, by induction on the derivation of \(\varnothing \vdash t : T\). Case on the last rule used.

• T-Var. Cannot occur. The context is empty, so \(x{:}T \in \varnothing\) is impossible. Vacuous.
• T-True, T-False, T-Abs. In each of these \(t\) is already a value (\(\texttt{true}\), \(\texttt{false}\), or an abstraction). The left disjunct holds immediately.
• T-App. Here \(t = t_1\,t_2\) with \(\varnothing \vdash t_1 : T_{11}\to T_{12}\) and \(\varnothing \vdash t_2 : T_{11}\). By the induction hypothesis on \(t_1\), if \(t_1 \to t_1'\), then E-App1 gives \(t_1\,t_2 \to t_1'\,t_2\), done. Otherwise \(t_1\) is a value, and by the IH on \(t_2\), if \(t_2 \to t_2'\) then E-App2 gives a step, done. Otherwise both are values. By the Canonical Forms Lemma clause (2), \(t_1 = \lambda x{:}T_{11}.\,t_{12}\), so \(t_1\,t_2\) is a beta-redex and E-AppAbs applies, giving \(t \to [x := t_2]\,t_{12}\). A step exists in every subcase.
• T-If. Here \(t = \texttt{if } t_1 \texttt{ then } t_2 \texttt{ else } t_3\) with \(\varnothing \vdash t_1 : \texttt{Bool}\). By the IH on \(t_1\), if it steps, E-If steps the whole term. If \(t_1\) is a value, Canonical Forms clause (1) makes it \(\texttt{true}\) or \(\texttt{false}\), and E-IfTrue or E-IfFalse fires. A step always exists.

Every case produces either a value or a step, so Progress holds. \(\blacksquare\) Notice where the type discipline earned its keep. Without the Canonical Forms Lemma, the T-App case could face a \(t_1\) that is a value but not a function (say \(\texttt{true}\)), and the term \(\texttt{true}\,\texttt{false}\) would be stuck. The type system forbids that term precisely so that the lemma holds.

Preservation

Theorem (Preservation). If \(\Gamma \vdash t : T\) and \(t \to t'\), then \(\Gamma \vdash t' : T\). Types are stable under reduction.

Beta substitutes a term into another, so preservation for E-AppAbs needs a lemma that substitution preserves typing, which in turn needs weakening.

Weakening. If \(\Gamma \vdash t : T\) and \(x\) is not in \(\Gamma\), then \(\Gamma, x{:}S \vdash t : T\). Proof. Induction on the derivation. Each rule's premises still hold with the extra, unused binding. \(\blacksquare\)

Substitution Lemma. If \(\Gamma, x{:}S \vdash t : T\) and \(\Gamma \vdash s : S\), then \(\Gamma \vdash [x := s]\,t : T\). Proof. Induction on the derivation of \(\Gamma, x{:}S \vdash t : T\), case on the last rule.

• T-Var, \(t = y\). If \(y = x\), then \(T = S\) and \([x:=s]\,x = s\), and \(\Gamma \vdash s : S\) is a premise, done. If \(y \neq x\), then \([x:=s]\,y = y\), and \(y{:}T \in \Gamma\), so T-Var still derives \(\Gamma \vdash y : T\).
• T-Abs, \(t = \lambda y{:}T_1.\,t_2\) with \(\Gamma, x{:}S, y{:}T_1 \vdash t_2 : T_2\). Rename so \(y \neq x\) and \(y\) is fresh for \(s\) (alpha-conversion, legitimate). Reorder the context and apply the IH to \(t_2\) under \(\Gamma, y{:}T_1, x{:}S\), giving \(\Gamma, y{:}T_1 \vdash [x:=s]\,t_2 : T_2\). Weakening supplies the binding for \(s\)'s typing. T-Abs concludes \(\Gamma \vdash \lambda y{:}T_1.\,[x:=s]\,t_2 : T_1 \to T_2\), which is \([x:=s]\,t\).
• T-App, \(t = t_1\,t_2\). The IH on both subderivations gives \(\Gamma \vdash [x:=s]\,t_1 : T_{11}\to T_{12}\) and \(\Gamma \vdash [x:=s]\,t_2 : T_{11}\), and T-App reassembles \(\Gamma \vdash [x:=s]\,(t_1\,t_2) : T_{12}\).
• T-True, T-False, T-If. Constants are unchanged by substitution and retype directly. For T-If the IH on the three subterms and one more use of T-If closes the case.

\(\blacksquare\) Now Preservation itself, by induction on the derivation of \(\Gamma \vdash t : T\), case on the last typing rule, using inversion on the step \(t \to t'\).

• T-Var, T-Abs, T-True, T-False. These type values or variables, and no reduction rule steps a value or a bare variable, so the hypothesis \(t \to t'\) is vacuously unavailable. Nothing to prove.
• T-App, \(t = t_1\,t_2\), \(\Gamma \vdash t_1 : T_{11}\to T_{12}\), \(\Gamma \vdash t_2 : T_{11}\), \(T = T_{12}\). Three reduction rules could have produced the step. For E-App1, \(t_1 \to t_1'\), and the IH gives \(\Gamma \vdash t_1' : T_{11}\to T_{12}\), so T-App reassembles \(\Gamma \vdash t_1'\,t_2 : T_{12}\). E-App2 is symmetric, using the IH on \(t_2\). For E-AppAbs, \(t_1 = \lambda x{:}T_{11}.\,t_{12}\) and \(t' = [x := t_2]\,t_{12}\). Inversion of T-Abs on the typing of \(t_1\) gives \(\Gamma, x{:}T_{11} \vdash t_{12} : T_{12}\). With \(\Gamma \vdash t_2 : T_{11}\), the Substitution Lemma yields \(\Gamma \vdash [x := t_2]\,t_{12} : T_{12}\), which is exactly \(\Gamma \vdash t' : T\). This is the case that consumes the whole lemma stack.
• T-If, \(t = \texttt{if } t_1 \texttt{ then } t_2 \texttt{ else } t_3\), \(\Gamma \vdash t_1 : \texttt{Bool}\), \(\Gamma \vdash t_2 : T\), \(\Gamma \vdash t_3 : T\). For E-IfTrue, \(t' = t_2\), and \(\Gamma \vdash t_2 : T\) is a premise. For E-IfFalse, \(t' = t_3\), premise again. For E-If, \(t_1 \to t_1'\), and the IH gives \(\Gamma \vdash t_1' : \texttt{Bool}\), so T-If rebuilds the conditional at type \(T\).

\(\blacksquare\) Combine the two. If \(\varnothing \vdash t : T\) and \(t \to^{*} t'\), iterated Preservation gives \(\varnothing \vdash t' : T\), and Progress applied to \(t'\) says \(t'\) is a value or steps again. So a well-typed closed term never reaches a stuck non-value, which is type soundness. A stuck term like \(\texttt{true}\,\texttt{false}\) is therefore untypable, and the proof is the guarantee that the type checker's rejections are never false alarms about safety. The same two-theorem shape, with product and sum and reference cases added, proves soundness for real languages. RustBelt is this argument carried out in the Iris separation logic for a language with mutable state and unsafe blocks.

Hindley-Milner and principal type inference

The simply-typed calculus demands an annotation on every \(\lambda\). ML and its descendants remove them entirely. The programmer writes \(\lambda x.\,t\) and the compiler reconstructs the most general type. The theory is Hindley's and Milner's, with Damas and Milner's 1982 paper giving the algorithm now called W and proving it computes principal types, meaning every other valid type for the term is an instance of the one it finds. Two ingredients make this work, unification to solve the equations the typing rules generate, and let-polymorphism to reuse a definition at several types.

Robinson's unification

A substitution \(\sigma\) maps type variables to types. Applying it, \(\sigma\,\tau\), replaces every variable in \(\tau\). Given two types \(\tau_1, \tau_2\), a unifier is a \(\sigma\) with \(\sigma\,\tau_1 = \sigma\,\tau_2\). Robinson (1965) proved that if a unifier exists, there is a most general one \(\sigma^{*}\), unique up to renaming, such that every unifier factors as \(\rho \circ \sigma^{*}\). The algorithm is structural recursion with an occurs check.

  unify(s, t):
    if s is a variable a:
        if t == a: return {}                       (nothing to do)
        if a occurs in t: FAIL  (occurs check: no finite type solves a = a->b)
        return { a := t }
    if t is a variable: unify(t, s)                 (symmetric)
    if s = C(s1..sn) and t = C(t1..tn):             (same constructor)
        sigma := {}
        for i in 1..n:
            sigma := unify(sigma(si), sigma(ti)) . sigma
        return sigma
    else: FAIL                                      (constructor clash)

The occurs check is the guard that keeps types finite. Unifying \(a\) with \(a \to b\) would demand an infinite type \((\dots \to b) \to b\), so it must fail. It is exactly the check that rejects self-application \(\lambda x.\,x\,x\), whose constraint is \(a = a \to b\). Constructor clash (\(\texttt{Bool}\) against an arrow, or a two-argument constructor against a three-argument one) is the other failure, and it is where an ordinary type error is reported.

Algorithm W, generalization, and let-polymorphism

Algorithm W walks the term, and at each node emits a constraint, solves it by unification, and threads the resulting substitution forward. A type scheme \(\sigma = \forall \alpha_1 \dots \alpha_n.\,\tau\) is a type with some variables marked polymorphic. Two operations connect schemes and types. Instantiation replaces the bound \(\alpha_i\) with fresh variables, so each use of a polymorphic value gets its own copy. Generalization, at a \(\texttt{let}\), closes over the variables free in the inferred type but not free in the environment.

The subtraction of \(\mathrm{ftv}(\Gamma)\) is the crucial restriction and the reason let-polymorphism is sound while "lambda-polymorphism" is not. A variable still tied to the environment, for example a \(\lambda\)-bound parameter currently being inferred, must not be generalized, because a later constraint may pin it down. Generalizing it early would let a single binding be used at two incompatible types and break soundness. This is why in ML \(\texttt{let}\) introduces polymorphism but a \(\lambda\) parameter is monomorphic within its body. It is also why the classic HM type system cannot type \(\lambda f.\,(f\,\texttt{true},\, f\,3)\). The parameter \(f\) is not at a \(\texttt{let}\), so it stays monomorphic and the two uses conflict. System F, below, lifts that restriction at the cost of decidable inference.

A principal type by hand for compose

Infer the type of \(\textsf{compose} = \lambda f.\lambda g.\lambda x.\, f\,(g\,x)\). Assign fresh variables to the three parameters, \(f : t_0\), \(g : t_1\), \(x : t_2\). Two applications generate two constraints.

The inner application \(g\,x\) forces \(g\) to be a function taking \(x\)'s type, so introduce a fresh result \(t_3\) and unify \(t_1\) with \(t_2 \to t_3\). The most general unifier is \(\{\, t_1 := t_2 \to t_3 \,\}\), and \(g\,x : t_3\).

The outer application \(f\,(g\,x)\) forces \(f\) to take \(t_3\), so introduce fresh \(t_4\) and unify \(t_0\) with \(t_3 \to t_4\). Unifier \(\{\, t_0 := t_3 \to t_4 \,\}\), and the body has type \(t_4\).

Reassemble through the three abstractions, applying the accumulated substitution \(\{\,t_0 := t_3 \to t_4, t_1 := t_2 \to t_3\,\}\).

Nothing constrains \(t_2, t_3, t_4\) further, so generalize all three. Renaming to \(a, b, c\) for readability gives the principal type

which is precisely what the runnable inferencer in the implementation section prints. The two substitution steps recorded there, t1 := t2 -> t3 and t0 := t3 -> t4, are the two unifications above. Every other valid type for compose, such as \((\texttt{Int}\to\texttt{Bool}) \to (\texttt{Char}\to\texttt{Int}) \to \texttt{Char} \to \texttt{Bool}\), is an instance of this scheme, which is the principal-types theorem made concrete.

Polymorphism, System F, and parametricity

Two things are called polymorphism and they are not the same. Parametric polymorphism is a single piece of code that works uniformly for every type, as \(\textsf{compose}\) above does. It cannot inspect the type it is instantiated at. Ad-hoc polymorphism, or overloading, is a family of different implementations selected by type, as with Haskell type classes, C++ templates with specialization, or Rust traits. The distinction matters because parametric code obeys strong laws that ad-hoc code does not.

System F, discovered independently by Girard (1972) in proof theory and Reynolds (1974) in programming languages, makes parametric polymorphism explicit. It adds type abstraction \(\Lambda \alpha.\, t\) and type application \(t\,[\tau]\), with universally quantified types \(\forall \alpha.\,\tau\). The polymorphic identity is \(\Lambda\alpha.\,\lambda x{:}\alpha.\,x\) of type \(\forall\alpha.\,\alpha\to\alpha\), and it is instantiated by supplying a type, so \((\Lambda\alpha.\,\lambda x{:}\alpha.\,x)[\texttt{Bool}]\) reduces to \(\lambda x{:}\texttt{Bool}.\,x\). System F is much more expressive than HM, but full type inference for it is undecidable (Wells, 1994), which is why practical languages use the HM fragment, where quantifiers appear only at the outside of a type (prenex or rank-1 polymorphism), and inference stays decidable.

Reynolds (1983) proved that parametric functions satisfy a relational property, and Wadler (1989) turned it into the slogan "theorems for free". The type of a parametric function alone, with no look at its code, implies equational laws it must obey. The canonical example is that any total function \(r : \forall \alpha.\, [\alpha] \to [\alpha]\) commutes with \(\textsf{map}\),

The intuition is simple. Because \(r\) may not inspect the elements, only shuffle, drop, or duplicate their positions, it cannot depend on what the elements are, so relabeling them with any \(h\) before or after \(r\) gives the same list. Reverse, take-the-first-three, and every other such function satisfies this for free from the type. Parametricity is also the theoretical content of "a value of type \(\forall\alpha.\,\alpha\to\alpha\) must be the identity" and underlies data abstraction, since a client that is parametric in a module's representation type cannot observe which representation was chosen.

Subtyping and variance

Subtyping adds a relation \(S <: T\), "every \(S\) is usable where a \(T\) is expected", with the subsumption rule that lets a term of the subtype flow into any position expecting the supertype.

The relation is reflexive and transitive. The only subtle rule is the one for function types, and getting its direction right is the single most tested piece of variance intuition.

Deriving the function-subtyping rule

When is \(S_1 \to S_2 <: T_1 \to T_2\)? By the meaning of \(<:\), it holds exactly when a value of type \(S_1 \to S_2\) can safely be used everywhere a \(T_1 \to T_2\) is expected. So imagine a context that has a \(T_1 \to T_2\)-shaped hole. That context will call the function with some argument it believes to be a \(T_1\), and will use the result as a \(T_2\). Substitute our \(S_1 \to S_2\) into the hole and ask what must hold for nothing to break.

• Arguments (contravariant). The context supplies a \(T_1\). Our function must accept it, so its declared domain \(S_1\) must be able to receive any \(T_1\), that is \(T_1 <: S_1\). The domain relation runs opposite to the whole-type relation. As functions get "smaller" in the subtype order, their argument types must get larger. This is contravariance.
• Results (covariant). The context uses whatever comes back as a \(T_2\). Our function returns an \(S_2\), so we need \(S_2 <: T_2\). Results run the same direction as the whole type. This is covariance.

The rule is a formal statement of the Liskov substitution principle. An override may weaken its preconditions (accept more, contravariant argument) and strengthen its postconditions (return less, covariant result). Getting the argument arrow backwards, treating function arguments as covariant, is precisely the unsoundness that let early Java and Eiffel array code fail at runtime, and it is why Rust and Scala make mutable containers invariant. A cell you can both read and write forces the element to be covariant (for reads) and contravariant (for writes) at once, and the only relation that is both is equality, so \(\textsf{Ref}\,S <: \textsf{Ref}\,T\) requires \(S = T\).

Algebraic data types and exhaustiveness

An algebraic data type is a sum of products. A value is one of several tagged variants, each carrying a tuple of fields. The canonical example is an option or a tree. In ML notation,

  type 'a tree = Leaf | Node of 'a tree * 'a * 'a tree

Sums are dual to products, and pattern matching is how a sum is eliminated. A match gives one branch per constructor, binding the fields. The type checker's exhaustiveness analysis, formalized by Maranget's algorithm and implemented in every ML-family compiler, computes whether the branches cover all constructors, and reports the missing pattern if not. This is a genuine safety property. An inexhaustive match is a partial function, a stuck state waiting to happen, and turning the warning into an error is how a compiler statically eliminates a class of runtime crashes. Sum types plus exhaustiveness are also why the ML family has no null. Absence is a constructor (None), and the checker forces every use to handle it, which is Hoare's "billion-dollar mistake" closed at the type level.

Effects and monads

A pure function's type promises it does nothing but compute a value. Real programs read files, mutate state, and fail. A monad, brought into programming by Moggi (1991) and Wadler (1992), is the type structure that threads such effects through pure code while keeping the types honest. A monad on a type constructor \(M\) is two operations,

"inject a pure value" and "bind", which runs a computation and feeds its result to the next. The three monad laws are what make this a reliable sequencing discipline rather than an arbitrary pair of functions.

The two identity laws say return is a unit for bind, adding no effect, only a value. Associativity is the load-bearing one. It says that how a sequence of effectful steps is grouped does not change its meaning, only their order does. That is exactly the guarantee needed to read \(m \mathbin{>\!\!>\!\!=} f \mathbin{>\!\!>\!\!=} g\) as a straight imperative sequence "do \(m\), then \(f\), then \(g\)", which is what Haskell's do-notation and the async/await sugar in many languages desugar to. The monad, then, is how a purely functional language recovers imperative sequencing without surrendering referential transparency. The effects are values of type \(M\,\alpha\), threaded in a fixed order by an operator that the laws guarantee behaves like a semicolon.

Linear and affine types, the theory under Rust

Ordinary type systems, including everything above, are governed by structural rules that treat a hypothesis in the context as reusable and discardable at will. Weakening lets an unused variable stay in the context, and contraction lets a variable be used twice. Girard's linear logic (1987), imported to programming by Wadler (1990), removes those rules. A linear type demands each value be used exactly once, with no weakening (may not discard) and no contraction (may not duplicate). An affine type keeps weakening but drops contraction, so a value may be used at most once, either consumed or dropped, but never used twice. Rust's ownership discipline is, at its core, an affine type system with a controlled escape hatch for borrowing.

Why affine types forbid use-after-move

Model a move as the affine typing rule for using a variable. In a structural system, the variable rule leaves the context intact, which is what silently licenses a second use. In the affine system, using a variable consumes it, splitting the context so the variable is no longer available afterward. Write the affine judgment with an explicit context split \(\Gamma_1, \Gamma_2\), where each hypothesis lives in exactly one half.

The variable rule types \(x\) only in the context that contains exactly \(x\), and the application rule partitions its context between the two subterms rather than sharing it. So a term that uses \(x\) twice, such as \(\textsf{pair}\,x\,x\), would need \(x\) in both halves of a split, which the partition forbids, so there is no derivation. Contraction is exactly the rule that would let one hypothesis serve both branches, and it has been removed. That absence is the whole content of "use after move is a type error". When Rust moves \(s\) into \(t\) with let t = s;, it has consumed the single affine permission for that value. A later s asks the context for a permission that is no longer there, and the checker rejects it. Because the type is affine rather than linear, dropping a value without using it is fine (weakening is retained), which is why Rust does not force every value to be consumed. It only forbids the second use.

The compiled evidence is in the implementation section. The program that moves a String and then reads it fails with rustc's error E0382, "borrow of moved value", and the program that clones before the second use, keeping every value to at most one consuming use, compiles and runs. Borrowing is the refinement that makes affine types tolerable to program in. A shared reference &T is a temporary, non-consuming use tracked by a region (a lifetime, below), and the borrow checker enforces the aliasing-xor-mutability invariant, at most one &mut or any number of &, that keeps the affine core sound in the presence of these temporary copies. RustBelt (Jung, Jourdan, Krebbers, and Dreyer, POPL 2018 and the extended JACM 2021 account) proved that this design, including the unsafe code inside the standard library that the safe type rules cannot themselves justify, is sound, by giving a semantic model of Rust types as ownership predicates in the Iris separation logic and showing each library's unsafe block satisfies the predicate its safe interface advertises. That is progress-and-preservation grown up, the same "well-typed cannot go wrong" statement, for a language with mutable aliasable memory and an unsafe escape hatch.

Regions, lifetimes, and gradual typing

The other half of Rust's memory story is where a value lives and for how long. Tofte and Talpin (1997) introduced region-based memory management. Instead of a garbage collector, the type system assigns each allocation to a region, a lexically scoped arena, and a region and everything in it are freed together when its scope ends. Their region inference computed these scopes automatically for an ML-like language, and the same idea, generalized to non-lexical scopes, appeared in Cyclone (Grossman and colleagues, 2002), the safe-C dialect that is Rust's direct ancestor. A Rust lifetime 'a is a region variable, and a borrow &'a T is a reference whose validity is confined to region 'a. The borrow checker is a region inference that rejects any reference escaping the region of the data it points into, which is how "dangling pointer" becomes a compile-time type error with no runtime cost.

Gradual typing addresses the opposite pressure, letting statically typed and dynamically typed code coexist in one program, so a codebase can migrate incrementally. Siek and Taha (2006) formalized a language with an unknown type \(\star\) and a consistency relation \(\sim\) that, unlike subtyping, is reflexive and symmetric but not transitive. Here \(\star \sim T\) for every \(T\), which lets dynamic values flow into typed contexts and back. The boundary between checked and unchecked code is mediated by casts, and a cast can fail at runtime when a dynamic value turns out not to match the static type it was promised to have. Wadler and Findler (2009) supplied the accountability story with blame. Every cast carries a label identifying which side of the boundary made the promise, and their theorem, "well-typed programs can't be blamed", proves that when a cast fails, blame always falls on the less-typed side of the boundary, never on the fully static code. That is the formal reason a type annotation is worth something even when part of the program is untyped. The typed fragment is exonerated in advance.

Memory safety across C, C++, Rust, and GC'd languages

The comparison that ties the theory together is what guarantee each language's type system actually delivers about memory, and at what cost. The table below is the honest summary.

The theory grounds every row. A garbage-collected language buys use-after-free safety by making the "free" invisible. The collector proves reachability at runtime, so no live pointer ever dangles, at the price of the collector itself. Rust buys the same safety statically, by making the type system carry the reachability argument at compile time through affine ownership and regions, so the free is inserted deterministically at the end of a value's single owner's scope, with no runtime tracing. C and C++ decline to encode the argument in types at all and leave it to the programmer, which is why their memory-safety record is what the security literature records and why the migration of systems code toward Rust is a direct, practical consequence of the type theory above. The data-race column is the same story one dimension over, and the concurrency page works it out in detail through Send and Sync.

Worked problems

  let v = vec![1, 2, 3];
  let a = sum(v);      // sum(v: Vec<i32>) -> i32  consumes v
  let b = sum(v);      // second use of v
  println!("{} {}", a, b);

Implementation

The theory is only convincing if it runs. The first block is a complete Hindley-Milner inferencer, Robinson unification plus Algorithm W with let-generalization, in dependency-free Python. It infers the principal type of compose, replays the two unification steps derived above, and rejects self-application on the occurs check. The output quoted underneath is the actual run.

from itertools import count

# ---- Types -----------------------------------------------------------------
class TVar:
    def __init__(self, name): self.name = name
    def __repr__(self): return self.name

class TApp:                       # applied constructor; "->" is a 2-arg TApp
    def __init__(self, con, args): self.con, self.args = con, args
    def __repr__(self):
        if self.con == "->" and len(self.args) == 2:
            a, b = self.args
            la = f"({a})" if isinstance(a, TApp) and a.con == "->" else f"{a}"
            return f"{la} -> {b}"
        return f"{self.con} " + " ".join(map(str, self.args))

def arrow(a, b): return TApp("->", [a, b])

class Scheme:                     # forall vars . type
    def __init__(self, vars, tipe): self.vars, self.tipe = vars, tipe

# ---- Substitution ----------------------------------------------------------
def apply(sub, t):
    if isinstance(t, TVar):
        return apply(sub, sub[t.name]) if t.name in sub else t
    if isinstance(t, TApp):
        return TApp(t.con, [apply(sub, a) for a in t.args])
    return t

def compose_sub(s2, s1):          # apply s1 then s2
    out = {k: apply(s2, v) for k, v in s1.items()}
    out.update({k: v for k, v in s2.items() if k not in out})
    return out

def ftv(t):
    if isinstance(t, TVar): return {t.name}
    if isinstance(t, TApp):
        s = set()
        for a in t.args: s |= ftv(a)
        return s
    return set()

# ---- Robinson unification --------------------------------------------------
class UnifyError(Exception): pass

def unify(t1, t2, trace):
    if isinstance(t1, TVar): return bind(t1, t2, trace)
    if isinstance(t2, TVar): return bind(t2, t1, trace)
    if t1.con != t2.con or len(t1.args) != len(t2.args):
        raise UnifyError(f"constructor clash: {t1} vs {t2}")
    s = {}
    for a, b in zip(t1.args, t2.args):            # decompose componentwise
        s = compose_sub(unify(apply(s, a), apply(s, b), trace), s)
    return s

def bind(v, t, trace):
    if isinstance(t, TVar) and t.name == v.name: return {}
    if v.name in ftv(t):                          # the occurs check
        raise UnifyError(f"occurs check: {v} in {t}")
    trace.append(f"{v.name} := {t}")
    return {v.name: t}

# ---- Algorithm W -----------------------------------------------------------
fresh = count()
def newvar(): return TVar(f"t{next(fresh)}")

def instantiate(sc):
    m = {v: newvar() for v in sc.vars}
    def go(t):
        if isinstance(t, TVar): return m.get(t.name, t)
        if isinstance(t, TApp): return TApp(t.con, [go(a) for a in t.args])
        return t
    return go(sc.tipe)

def generalize(env, t):
    bound = set().union(*[ftv(s.tipe) - set(s.vars) for s in env.values()]) if env else set()
    return Scheme(sorted(ftv(t) - bound), t)      # close over vars not in env

# expression AST: ('var',x) ('lam',x,body) ('app',f,a) ('let',x,e1,e2)
def infer(env, e, sub, trace):
    if e[0] == 'var':
        return sub, instantiate(env[e[1]])
    if e[0] == 'lam':
        _, x, body = e
        tv = newvar(); env2 = {**env, x: Scheme([], tv)}
        sub, tb = infer(env2, body, sub, trace)
        return sub, arrow(apply(sub, tv), tb)
    if e[0] == 'app':
        _, f, a = e
        sub, tf = infer(env, f, sub, trace)
        sub, ta = infer(env, a, sub, trace)
        tr = newvar()
        sub = compose_sub(unify(apply(sub, tf), arrow(ta, tr), trace), sub)
        return sub, apply(sub, tr)
    if e[0] == 'let':                             # generalize e1 before binding
        _, x, e1, e2 = e
        sub, t1 = infer(env, e1, sub, trace)
        env2 = {**env, x: generalize(env, apply(sub, t1))}
        return infer(env2, e2, sub, trace)

def principal(e, env=None):
    global fresh; fresh = count()
    trace = []
    sub, t = infer(env or {}, e, {}, trace)
    return apply(sub, t), trace

def rename(t, m=None, it=None):                   # tidy vars to a, b, c, ...
    m = {} if m is None else m; it = iter("abcdefghij") if it is None else it
    if isinstance(t, TVar):
        if t.name not in m: m[t.name] = TVar(next(it))
        return m[t.name]
    if isinstance(t, TApp): return TApp(t.con, [rename(a, m, it) for a in t.args])
    return t

# compose = \f.\g.\x. f (g x)
compose = ('lam','f',('lam','g',('lam','x',
          ('app',('var','f'),('app',('var','g'),('var','x'))))))
t, tr = principal(compose)
print("compose :", rename(t))
for s in tr: print("  step:", s)

selfapp = ('lam','x',('app',('var','x'),('var','x')))   # \x. x x
try: principal(selfapp)
except UnifyError as ex: print("self-application rejected:", ex)

-- The same three types expressed where the compiler infers them for you.
-- Haskell (GHC): principal types are reported by :t with no annotations.

compose :: (b -> c) -> (a -> b) -> a -> c
compose f g x = f (g x)

twice :: (a -> a) -> a -> a          -- Problem 1's term; note a -> a domain
twice f x = f (f x)

-- A sum type with exhaustive pattern matching; -Wincomplete-patterns
-- turns a missing case into a warning (an error with -Werror).
data Tree a = Leaf | Node (Tree a) a (Tree a)

size :: Tree a -> Int
size Leaf           = 0
size (Node l _ r)   = 1 + size l + size r      -- both constructors covered

-- The Maybe monad: return and bind satisfy the three monad laws, which is
-- why do-notation reads as an imperative sequence that may short-circuit.
safeDiv :: Int -> Int -> Maybe Int
safeDiv _ 0 = Nothing
safeDiv a b = Just (a `div` b)

chain :: Int -> Int -> Int -> Maybe Int
chain a b c = safeDiv a b >>= \q -> safeDiv q c   -- Nothing propagates

// Affine ownership, checked by rustc. This file is two programs:
// the first fails to type-check (use-after-move), the second compiles.

// ---- FAILS: rustc rejects this with error[E0382] ----
// fn main() {
//     let s = String::from("owned");
//     let t = s;            // move: the single permission passes to t
//     println!("{}", s);    // error[E0382]: borrow of moved value: `s`
//     println!("{}", t);
// }

// ---- COMPILES and RUNS: each value consumed at most once ----
#[derive(Clone)]
struct Buf { data: Vec<u8> }

fn consume(b: Buf) -> usize { b.data.len() }   // takes ownership (affine use)

fn main() {
    let b = Buf { data: vec![1, 2, 3] };
    let n = consume(b.clone());   // clone: a fresh permission is consumed
    let m = consume(b);           // last use of b: moved exactly once
    println!("{} {}", n, m);      // prints: 3 3
}

Running the Python inferencer prints the principal type and the two substitution steps, then the occurs-check rejection, matching the derivation above exactly.

  compose : (a -> b) -> (c -> a) -> c -> b
    step: t1 := t2 -> t3
    step: t0 := t3 -> t4
  self-application rejected: occurs check: t0 in t0 -> t1

The Rust file was compiled with rustc --edition 2021. The commented-out first main is the use-after-move. When it is the active program, the compiler produces

  error[E0382]: borrow of moved value: `s`
   --> move_fail.rs:4:20
    |
  3 |     let t = s;              // move: ownership transfers to t
    |             - value moved here
  4 |     println!("{}", s);      // error: s used after move
    |                    ^ value borrowed here after move

and the second main, the one shown active, compiles cleanly and prints 3 3. The affine typing rule of Problem 4 is not a metaphor for what the compiler does. It is what the compiler does.

How it is done in practice

Production type checkers depart from the textbook algorithm in ways that are worth knowing. Real HM implementations do not build substitutions as dictionaries and compose them. They use the union-find data structure, representing each type variable as a mutable cell that is destructively unified by pointer-linking, which turns the whole inference into a near-linear-time pass. OCaml's inferencer and GHC's are both union-find at heart, and GHC's is wrapped in the constraint-solving architecture of the "OutsideIn(X)" system (Vytiniotis, Peyton Jones, Schrijvers, and Sulzmann) that reconciles inference with GADTs and type families, features that break the clean principal-types guarantee and force the compiler to demand annotations at exactly the points where principality is lost.

The error-message problem is where most of the engineering goes. The naive algorithm reports a unification failure at whatever node the substitution finally became inconsistent, which is frequently far from the programmer's actual mistake. A decade of work on improving these messages, from Lerner and colleagues' counterfactual typing to the localized-blame heuristics in Elm and Rust, is aimed at reporting the cause rather than the symptom. Rust's borrow checker went through the same maturation. The original lexical version (AST-based) rejected sound programs whose borrows did not fit lexical scopes, and the non-lexical lifetimes redesign (NLL), which computes liveness on the control-flow graph in the manner the compilers and program analysis page develops for dataflow, accepted them while keeping soundness. The lesson repeated across all of these systems is that a type system's theory fixes what is possible to accept soundly, and years of implementation work are spent making the checker accept as much of that as it can and explain the rest.

The current research frontier

Four threads are active. The first is mechanized soundness. The RustBelt line at MPI-SWS built its proofs in the Iris separation logic inside Coq, and the same group's later work (RustBelt Meets Relaxed Memory, and the GhostCell and RustHornBelt papers) pushes the machine-checked account to weak memory and to verified functional correctness of Rust code, not just safety. CompCert and the CakeML verified compiler are the compiler-side analogues, proving that the semantics preserved by the type system survives translation to machine code. The second is ownership beyond Rust. Linear and affine types are being retrofitted into languages that were not designed for them, with GHC's LinearTypes extension (Bernardy, Boespflug, Newton, Peyton Jones, and Spiwack) and the ownership experiments in newer languages like Roc and Austral, exploring how much of Rust's guarantee is achievable with a garbage collector still present for the non-linear parts.

Third, gradual typing at scale, where the open problem is the runtime cost of the casts at the static/dynamic boundary. The "gradual guarantee" of Siek, Vitousek, Cimini, and Boyland formalizes what a sound gradual system must preserve as annotations are added or removed, and Takikawa and colleagues' performance study of Typed Racket showed the tax can be catastrophic in the worst case, which has driven work on faster sound representations (transient and monotonic semantics) and is directly relevant to how TypeScript, which is deliberately unsound and erases its types, trades the guarantee away for zero runtime cost. Fourth, and most visibly, there are types for machine learning. Shape-checking tensor programs at compile time is an old dependent-types idea now urgent because a shape mismatch in a training run is expensive, with dependent and refinement-typed approaches appearing across research systems and in the type stubs the Python typing community is standardizing. The through-line is that the metatheory in this page, soundness, parametricity, and the affine discipline, is the toolkit each of these frontiers reaches for.

Open source to read

• rust-lang/rust: the borrow checker and region inference. Open compiler/rustc_borrowck/ for the NLL implementation. The affine move-checking lives in rustc_mir_dataflow. This is affine types and regions as production code.
• ghc/ghc: the most complete open HM-plus-extensions inferencer. Start in compiler/GHC/Tc/ (the typechecker) and GHC/Core/Unify.hs for unification. The constraint solver is the OutsideIn engine.
• ocaml/ocaml: a famously readable union-find inferencer. typing/ctype.ml is unification by destructive variable linking, the algorithm production compilers actually use.
• microsoft/TypeScript: structural subtyping and a deliberately unsound gradual system at enormous scale. src/compiler/checker.ts is the single largest type checker in wide use. Read its isTypeAssignableTo for structural subtyping in practice.
• WebAssembly/spec: the reference interpreter alongside a fully formal small-step semantics and type system, one of the few industrial languages whose soundness is proved on paper (Watt's mechanization) against the very interpreter shipped. Read interpreter/.
• roc-lang/roc: a modern pure functional language whose compiler uses opportunistic in-place mutation guided by ownership inference, a working example of affine reasoning under a functional surface. The crates/compiler/ tree holds the inferencer.
• plfa/plfa.github.io: "Programming Language Foundations in Agda", the progress and preservation proofs of this page written as machine-checked Agda. The best way to be sure the STLC soundness argument has no gaps is to read it there.

Common misconceptions

"A sound type system means the program is correct." Soundness means only that a well-typed program does not reach a stuck state the semantics leaves undefined, that the operations it performs are the ones their types promise. It says nothing about whether the program computes the intended function. A sorting routine that returns its input unchanged is perfectly well-typed. Progress and preservation guarantee "does not go wrong", not "does the right thing".

"Type inference and dynamic typing are opposites." They are orthogonal. Hindley-Milner is fully static and yet requires no annotations at all, which is why ML feels as annotation-light as a dynamic language while checking everything at compile time. The absence of written types is inference, not dynamism.

"Function arguments should be covariant, like results." This is the most common variance error and it is unsound. An override or a subtype function must accept at least everything the supertype accepts, so its argument type must be larger, contravariant. Treating arguments as covariant is exactly the hole that made Java's covariant arrays throw ArrayStoreException at runtime.

"Rust's borrow checker is a garbage collector done at compile time." It is not a collector at all. A collector proves reachability at runtime and frees whatever is unreachable. The borrow checker proves, statically, that each value has a single owner and inserts the free deterministically at the owner's scope end. There is no tracing, no runtime bookkeeping, and no pause. The guarantee comes from affine types and regions, not from reachability analysis.

"The occurs check is an optimization." It is a soundness requirement. Without it, unification would happily solve \(a = a \to b\) with an infinite type, and terms like \(\lambda x.\,x\,x\) would be accepted, breaking the correspondence between types and finite values. Some deliberately extended systems (equirecursive types) drop it on purpose, but then they add explicit machinery to keep the types meaningful.

"Monads are about side effects." Monads are a general interface for sequencing computations that satisfy three laws. Effects are one important instance. Maybe sequences possibly-failing computations, list sequences nondeterministic ones, and the parser monad sequences consumption of input, none of which is a side effect. What all monads share is the associativity law that makes "then" unambiguous.

"TypeScript is sound, so its types catch all type errors." TypeScript is intentionally unsound in several places (bivariant method parameters, unchecked index access historically, and any) and erases all types before running, so a value can violate its static type at runtime with no check. It buys developer productivity by giving up the soundness theorem, which is a legitimate engineering choice, but it is not the guarantee that OCaml or Rust make.

Self-check

References

1. Pierce, B. C. Types and Programming Languages. MIT Press, 2002. The standard reference. The progress-and-preservation proof of this page follows its presentation of the simply-typed lambda calculus.
2. Harper, R. Practical Foundations for Programming Languages, 2nd ed. Cambridge University Press, 2016. project page.
3. Winskel, G. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993.
4. Nielson, H. R., and Nielson, F. Semantics with Applications: An Appetizer. Springer, 2007 (orig. 1992).
5. Milner, R. A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences 17(3), 1978. Introduces Algorithm W. DOI.
6. Damas, L., and Milner, R. Principal Type-Schemes for Functional Programs. POPL, 1982. Proves W computes principal types. DOI.
7. Hindley, R. The Principal Type-Scheme of an Object in Combinatory Logic. Transactions of the AMS 146, 1969.
8. Robinson, J. A. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM 12(1), 1965. The unification algorithm. DOI.
9. Reynolds, J. C. Towards a Theory of Type Structure. Programming Symposium (Paris), Springer LNCS 19, 1974. System F, independently of Girard.
10. Girard, J.-Y. Interpretation fonctionnelle et elimination des coupures de l'arithmetique d'ordre superieur. PhD thesis, Universite Paris VII, 1972. The polymorphic lambda calculus (System F).
11. Reynolds, J. C. Types, Abstraction and Parametric Polymorphism. IFIP Congress, 1983. The relational parametricity theorem.
12. Wadler, P. Theorems for Free! FPCA, 1989. Free theorems from parametricity. DOI.
13. Moggi, E. Notions of Computation and Monads. Information and Computation 93(1), 1991. DOI.
14. Wadler, P. The Essence of Functional Programming. POPL, 1992. Monads for effects and the monad laws. DOI.
15. Wadler, P. Linear Types Can Change the World! Programming Concepts and Methods, 1990. Linear types for programming.
16. Wright, A. K., and Felleisen, M. A Syntactic Approach to Type Soundness. Information and Computation 115(1), 1994. Progress plus preservation. DOI.
17. Church, A. A Formulation of the Simple Theory of Types. Journal of Symbolic Logic 5(2), 1940. DOI.
18. Tofte, M., and Talpin, J.-P. Region-Based Memory Management. Information and Computation 132(2), 1997. DOI.
19. Grossman, D., Morrisett, G., Jim, T., Hicks, M., Wang, Y., and Cheney, J. Region-Based Memory Management in Cyclone. PLDI, 2002. DOI.
20. Siek, J. G., and Taha, W. Gradual Typing for Functional Languages. Scheme and Functional Programming Workshop, 2006.
21. Wadler, P., and Findler, R. B. Well-Typed Programs Can't Be Blamed. ESOP, 2009. DOI.
22. Jung, R., Jourdan, J.-H., Krebbers, R., and Dreyer, D. RustBelt: Securing the Foundations of the Rust Programming Language. POPL, 2018, extended in Journal of the ACM 66(1), 2021. DOI.
23. Vytiniotis, D., Peyton Jones, S., Schrijvers, T., and Sulzmann, M. OutsideIn(X): Modular Type Inference with Local Assumptions. Journal of Functional Programming 21(4-5), 2011. DOI.
24. Takikawa, A., Feltey, D., Greenman, B., New, M. S., Vitousek, J., and Felleisen, M. Is Sound Gradual Typing Dead? POPL, 2016. DOI.