2. Normalization by Evaluation and Bidirectional Typing

But what on earth do we think we’re doing in the first place? What’s our game? We have the ways of making things, but things are evidence. Perhaps, one day, the thing we’ll make is sense.

The story resumes where chapter 1 stopped: a tree and a question. The tree is Raw, the named syntax of the object language; the question was why let demands a type annotation while a lambda may go without. This chapter builds the type checker that answers it, and the checker needs two ingredients that are interesting in their own right: a way to decide definitional equality, because in a dependent type theory types contain programs and comparing types means comparing what programs compute; and a discipline for where types flow, because some terms announce their types and some can only be judged against one. The first ingredient is normalization by evaluation; the second is bidirectional typing.

Rules before algorithms

Before any implementation, a type theory is a system of rules. The nLab's article on type theory states the convention plainly: "Generally, a type theory is formulated by the rules called natural deduction, which declare the nature of each kind of type by a 4-step rule":

• type formation rules, "which say on which basis a new type can be introduced";
• term introduction rules, "which say how that new type can be inhabited by terms";
• term elimination rules, "which say how from a term of the new type one gets terms of other types";
• computation rules, "which constrain the result of combining term introduction with term elimination".

The object language of these lectures has exactly two kinds of type, Pi and Unit, plus the universe U they inhabit, so the whole specification fits on a page. Readers meeting rules of this shape for the first time will find them developed at a textbook's pace, lambda calculus first, in Nederpelt and Geuvers' Type Theory and Formal Proof. Here is the specification, every rule wearing its name on the right. Pi carries the full four steps, and a fifth kind the four-step scheme leaves optional, the uniqueness rule, better known as eta:

The type Unit is the same scheme with most steps empty: it can be formed, its one term can be introduced, and nothing eliminates it. With no eliminator there is nothing for a computation rule to constrain, and the uniqueness rule carries the whole weight, which is why it returns twice below, once inside quotation and once as the most type-dependent case of conversion:

What remains is plumbing: the universe's own formation rule, the variable rule, the rule for let, and the conversion rule that lets a term change into any type definitionally equal to the one it has. The first of these is the U : U shortcut, whose price a later section pays honestly:

One thing these rules are not is an algorithm. They say which judgments hold, not how to decide one, and read as a procedure they are nondeterministic in two ways. The rule Conv applies to every term at every moment, so a naive search never knows when to convert; and in Π-intro read bottom-up, the premise mentions the types $A$ and $B$ while the bare lambda being judged spells neither. Rules, by default, define a relation. Bidirectional typing, the subject of this chapter's second half, is the standard first step from the relation toward an algorithm: fix, for every judgment, which parts are inputs and which are outputs, and the nondeterminism drains out. The section on bidirectional typing lists every rule above a second time, moded, so the two readings can be compared side by side.

Names become indices

The named tree is wrong for checking. Deciding whether \x. x and \y. y are the same program should not depend on the letters chosen, and substitution under binders with names invites capture. The standard cure is de Bruijn's: a variable is not a name but a number counting how many binders sit between the variable and the one that bound it. The core language:

inductive Tm where
  | var (i : Nat)
  | univ
  | unitType
  | unitElem
  | lam (x : String) (dom? : Option Tm) (body : Tm)
  | app (fn arg : Tm)
  | pi (x : String) (dom cod : Tm)
  | letE (x : String) (ty val body : Tm)
deriving Repr

/-- Binder names are printing hints, so equality must not see them; a derived
`BEq` would compare the strings and mistake spelling for meaning. -/
def Tm.alphaEq : Tm -> Tm -> Bool
  | .var i, .var j => i == j
  | .univ, .univ => true
  | .unitType, .unitType => true
  | .unitElem, .unitElem => true
  | .lam _ none body, .lam _ none body' => body.alphaEq body'
  | .lam _ (some dom) body, .lam _ (some dom') body' =>
    dom.alphaEq dom' && body.alphaEq body'
  | .app fn arg, .app fn' arg' => fn.alphaEq fn' && arg.alphaEq arg'
  | .pi _ dom cod, .pi _ dom' cod' => dom.alphaEq dom' && cod.alphaEq cod'
  | .letE _ ty val body, .letE _ ty' val' body' =>
    ty.alphaEq ty' && val.alphaEq val' && body.alphaEq body'
  | _, _ => false

instance : BEq Tm :=
  ⟨Tm.alphaEq⟩

A var 0 refers to the nearest enclosing binder, var 1 to the one behind it, and so on. Binder names survive only as strings for printing; the binding structure is entirely in the numbers, so alpha-equivalence collapses into equality of trees, the printing names aside. That aside is the one care owed: a derived BEq would compare the printing names too and mistake spelling for meaning, so the instance is written by hand to ignore exactly that field. The n-Category Café essay under Further reading reconstructs this representation from first principles, as the thing one would invent when bookkeeping under renaming becomes unbearable. Note also what this chapter does not build: there is no separate scope-checking pass from Raw to Tm. Resolving a name means finding its binder, and in a dependent language the checker must look up the binder's type at exactly that moment, so scope resolution lives inside the checker, fused with typing.

Values, closures, and the neutral

To compare programs by what they compute, the checker needs to run them. Running produces values:

mutual

inductive Val where
  | univ
  | unitType
  | unitElem
  | lam (x : String) (clo : Closure)
  | pi (x : String) (dom : Val) (cod : Closure)
  | neutral (ty : Val) (ne : Neutral)

inductive Neutral where
  | var (lvl : Nat)
  | app (fn : Neutral) (arg : Val) (argTy : Val)

inductive Closure where
  | mk (env : List Val) (body : Tm)

end

instance : Inhabited Val where
  default := .univ

Three decisions live in this definition. First, a lambda value does not carry an evaluated body; it carries a Closure, the unevaluated body together with the environment it was written in. Evaluation stops at binders and resumes only when an argument arrives. Second, open terms force a new kind of value: under a binder, a variable has no entry in any environment, and a term stuck on such a variable is a neutral. Christiansen's tutorial puts it plainly: a neutral expression is one we cannot yet reduce, because information such as a function's argument is not yet known. We follow the tutorial in making Neutral its own type, a variable under a spine of applications, so that "stuck" is a definition rather than a convention; elaboration-zoo, by contrast, inlines the two neutral cases directly into its value type. Third, every neutral carries its type, and every argument in the spine carries its own: quotation below is type-directed, and these annotations are what it directs itself by.

One more representation choice hides in Neutral.var: it holds a level, not an index. An index counts binders from the inside out and is stable when a term is placed under new binders; a level counts from the outside in and is stable on the other side, when new binders grow around an environment. Values live in environments, so values use levels; terms use indices; quotation converts.

The two countings are easiest to compare on one untyped term, the S combinator, with every occurrence colored by its binder. An index counts enclosing lambdas outward from the occurrence to its binder; a level numbers the lambdas from the outside in, so the same occurrence generally wears different numbers:

The S combinator is a gentle case, because its three binders nest in a single telescope: every occurrence sits under all of them. The countings truly part ways on a term whose binders branch, the worked example of Wikipedia's article on de Bruijn indices, redrawn here with our zero-based counting and an arrow from each occurrence to its binder. Named, the term is $\lambda z.\; (\lambda y.\; y\; (\lambda x.\; x))\; (\lambda w.\; z\; w)$. An index is a distance: stand at the occurrence and count the lambdas crossed on the way out, before reaching the one that binds. The occurrence of $z$ crosses one lambda, so it wears 1; the other three occurrences bind to the nearest enclosing lambda and all wear 0:

A level is an address: count the lambdas from the root down to the binder, before reaching it. The outermost lambda is address 0 from wherever it is referenced; the two sibling lambdas in the branches are both 1; the innermost is 2:

Same term, same arrows: the binding structure never moves, and only the numerals on it change. Indices let distinct variables share a numeral, as the three zeros above do; levels give each binder one number for good, wherever it is referenced. The two countings meet in a subtraction that can be checked against the picture: an occurrence under $n$ binders referring to level $l$ has index $n - l - 1$, so the occurrence of $z$, under two binders at level 0, has index 1. Quotation below performs exactly this subtraction.

mutual

partial def Closure.apply : Closure -> Val -> Val
  | .mk env body, v => eval (v :: env) body

partial def applyVal : Val -> Val -> Val
  | .lam _ clo, v => clo.apply v
  | .neutral (.pi _ dom cod) ne, v => .neutral (cod.apply v) (.app ne v dom)
  | _, _ => default

partial def eval (env : List Val) : Tm -> Val
  | .var i => env.getD i default
  | .univ => .univ
  | .unitType => .unitType
  | .unitElem => .unitElem
  | .lam x _ body => .lam x (.mk env body)
  | .pi x dom cod => .pi x (eval env dom) (.mk env cod)
  | .app fn arg => applyVal (eval env fn) (eval env arg)
  | .letE _ _ val body => eval (eval env val :: env) body

end

The evaluator is a dozen lines. Application either enters a closure or, when the function is neutral, grows the spine, computing the result type from the Pi's codomain closure; let evaluates its definition and extends the environment, and a variable is a lookup. The definition is honestly partial, as in chapter 1: our object language has U : U, and a theory with a universe of all types admits terms with no normal form, so no termination proof exists to be found.

Quotation, and two eta laws

Values compute fast but cannot be compared directly, since closures capture environments. The way back is quotation: read a value back into a term, opening every binder with a fresh neutral variable. Reading a level back into an index is one subtraction, and a quiet trap:

def lvlToIx (lvl k : Nat) : Nat :=
  lvl - k - 1

Natural-number subtraction in Lean truncates at zero, so an out-of-scope level does not crash here; it silently produces a wrong index. The checker never feeds quote such a level, but the function's type does not say so, and an honest remark is owed: this is an invariant carried in the programmer's head, exactly the kind of debt chapter 6 pays off with intrinsic typing.

mutual

partial def quote (lvl : Nat) (ty v : Val) : Tm :=
  match ty with
  | .pi x dom cod =>
    let fresh := Val.neutral dom (.var lvl)
    .lam x none (quote (lvl + 1) (cod.apply fresh) (applyVal v fresh))
  | .unitType => .unitElem
  | _ =>
    match v with
    | .univ => .univ
    | .unitType => .unitType
    | .pi x dom cod =>
      let fresh := Val.neutral dom (.var lvl)
      .pi x (quote lvl .univ dom) (quote (lvl + 1) .univ (cod.apply fresh))
    | .neutral _ ne => quoteNeutral lvl ne
    | _ => default

partial def quoteNeutral (lvl : Nat) : Neutral -> Tm
  | .var k => .var (lvlToIx lvl k)
  | .app ne arg argTy => .app (quoteNeutral lvl ne) (quote lvl argTy arg)

end

The shape of quote is the chapter's second lesson, and it comes from Christiansen: reading back is recursive on the structure of the type, not the value. At a Pi type, every value reads back with a lambda on top, whether or not it is one; applying the value to a fresh neutral and quoting the result is precisely the eta law for functions, performed rather than checked. At Unit, the value is not even inspected: everything of type Unit reads back as unit, the eta law for the one-valued type. Only at a universe or a stuck type does quotation fall back to the structure of the value. This is where the type annotations on neutrals earn their keep: quoting a spine argument needs the type to quote it at.

def nf (env : List Val) (ty : Val) (t : Tm) : Tm :=
  quote 0 ty (eval env t)

def conv (lvl : Nat) (ty v w : Val) : Bool :=
  quote lvl ty v == quote lvl ty w

Conversion checking, the heart of a dependent type checker, is then two lines: normalize both sides at their common type and compare trees, alpha-equivalence being free with de Bruijn. The eta laws need no cases of their own because quotation already performed them. Elaboration-zoo makes the other classic choice, an untyped structural recursion on pairs of values with two asymmetric cases for a lambda facing a non-lambda; it never needs the types, but it also cannot support a law like Unit's, where equality holds by virtue of the type alone. The difference is the most dependently-typed lesson in this chapter: definitional equality is not one relation, it is a family indexed by types.

Bidirectional typing

With conversion decided, typing remains. The discipline: some terms synthesize a type, written $\Gamma \vdash t \mathrel{\textcolor{#0f4c81}{\Rightarrow}} A$, and some can only inherit a given one, written $\Gamma \vdash t \mathrel{\textcolor{#cf222e}{\Leftarrow}} A$. Constructors are the inheriting kind. A bare unit could inhabit any one-element type a language might have, and a bare lambda names its variable but not its domain; both are introduction forms, and introduction forms answer to expectations. Eliminations synthesize: a variable's type is in the context, and an application's type comes out of the function's. The two judgments meet in one rule, the mode switch: when a term that prefers to synthesize must inherit, synthesize and then ask conversion whether the types agree.

One notation, three problems. A judgment relates a context, a term, and a type: a triplet. Which of the three is unknown decides what kind of problem the judgment states, and the table deliberately writes the triplet with the neutral colon rather than with either arrow, because the arrows belong to the two modes this chapter implements, and reusing the synthesis arrow for the third row would suggest that proof search is one more mode of the same algorithm. It is not:

The first two rows are this chapter. The third, finding a program from its type, is proof search, a different subject entirely, and the table earns its place by locating it: one judgment form, three problems, told apart only by what is unknown. A word on words is owed here. The red arrow, pointing into the term, resembles a letter C, and much of the literature says checking for that mode and inference for the blue one; these lectures avoid both, because each word is already claimed several times over. Checking names the whole program, the type checker, and the conversion checking inside it; inference names Hindley–Milner's different game below. The implementation is a type checker, the discipline is typing, and the two modes are inheritance and synthesis, nothing else.

The promise of the opening section can now be kept: here is every rule of the object language a second time, the undirected original on the left, the moded version on the right, the rule's name at the far right. Introductions inherit, and everything that can name its own type, variables, formations, eliminations, synthesizes:

Three observations pay for the duplication. The rule Conv, undirected, was the one applicable everywhere; moded, it fires at exactly one spot, where a synthesizing term meets an inheriting position, and it is the only rule that changes direction. The rule Π-intro-ann has no original: the annotated lambda exists in the grammar precisely so that a lambda can synthesize when no expectation is available, the grammar paying for the algorithm. And the opening section's computation rule appears nowhere at all: Π-comp moved, and the two uniqueness rules with it, inside the $\equiv$ premise of Conv, which is the conversion checking that normalization by evaluation decides. Rules that constrain never became rules that run; they became the equality the mode switch consults. The rule Π-elim is also where dependency bites: the argument that just inherited its type is substituted into the codomain, which in NbE clothing means applying the codomain closure to the argument's value. The context that supports all this keeps the typing information and the evaluation environment side by side, with one split worth naming: entering a binder pushes an opaque neutral, entering a let pushes the actual value, and that is the entire difference between a variable and a definition.

structure Cxt where
  env : List Val
  types : List (String × Val)
  lvl : Nat

def Cxt.empty : Cxt :=
  ⟨[], [], 0⟩

/-- Enter a binder: the variable is opaque, so the environment gets a
neutral. -/
def Cxt.bind (cxt : Cxt) (x : String) (ty : Val) : Cxt :=
  ⟨.neutral ty (.var cxt.lvl) :: cxt.env, (x, ty) :: cxt.types, cxt.lvl + 1⟩

/-- Enter a definition: the variable has a value, and evaluation may use
it. -/
def Cxt.define (cxt : Cxt) (x : String) (v ty : Val) : Cxt :=
  ⟨v :: cxt.env, (x, ty) :: cxt.types, cxt.lvl + 1⟩

def Cxt.lookup (cxt : Cxt) (x : String) : Option (Nat × Val) :=
  go 0 cxt.types
where
  go (i : Nat) : List (String × Val) -> Option (Nat × Val)
    | [] => none
    | (y, ty) :: rest => if x == y then some (i, ty) else go (i + 1) rest

The checker itself is a page. Inheritance has exactly three interesting cases, the two constructors and let, and the mode-switch fallthrough; elaboration-zoo's source whose language has no Unit, states its two-case version as a comment, "only Lam and Let is checkable".

mutual

partial def inherit (cxt : Cxt) : Raw -> Val -> Except String Tm
  | .lam x none body, .pi _ dom cod => do
    let fresh := Val.neutral dom (.var cxt.lvl)
    let body' <- inherit (cxt.bind x dom) body (cod.apply fresh)
    pure (.lam x none body')
  | .unitElem, .unitType => pure .unitElem
  | .letE x ty val body, expected => do
    let ty' <- inherit cxt ty .univ
    let vty := eval cxt.env ty'
    let val' <- inherit cxt val vty
    let body' <- inherit (cxt.define x (eval cxt.env val') vty) body expected
    pure (.letE x ty' val' body')
  | t, expected => do
    let (t', synthesized) <- synth cxt t
    if conv cxt.lvl .univ synthesized expected then
      pure t'
    else
      throw s!"type mismatch: expected {showTy cxt expected}, \
        found {showTy cxt synthesized}"

partial def synth (cxt : Cxt) : Raw -> Except String (Tm × Val)
  | .var x =>
    match cxt.lookup x with
    | some (i, ty) => pure (.var i, ty)
    | none => throw s!"unknown variable {x}"
  | .univ => pure (.univ, .univ)
  | .unitType => pure (.unitType, .univ)
  | .pi x dom cod => do
    let dom' <- inherit cxt dom .univ
    let cod' <- inherit (cxt.bind x (eval cxt.env dom')) cod .univ
    pure (.pi x dom' cod', .univ)
  | .app fn arg => do
    let (fn', fnTy) <- synth cxt fn
    match fnTy with
    | .pi _ dom cod => do
      let arg' <- inherit cxt arg dom
      pure (.app fn' arg', cod.apply (eval cxt.env arg'))
    | _ => throw s!"expected a function, found something of type \
        {showTy cxt fnTy}"
  | .lam x (some dom) body => do
    let dom' <- inherit cxt dom .univ
    let vdom := eval cxt.env dom'
    let (body', bodyTy) <- synth (cxt.bind x vdom) body
    pure (.lam x (some dom') body',
      .pi x vdom (.mk cxt.env (quote (cxt.lvl + 1) .univ bodyTy)))
  | .lam _ none _ =>
    throw "cannot synthesize the type of an unannotated lambda; \
      annotate the binder, or let it inherit an expected type"
  | .unitElem =>
    throw "cannot synthesize the type of a bare constructor; \
      unit inherits its type, never synthesizes it"
  | .letE x ty val body => do
    let ty' <- inherit cxt ty .univ
    let vty := eval cxt.env ty'
    let val' <- inherit cxt val vty
    let (body', bodyTy) <- synth (cxt.define x (eval cxt.env val') vty) body
    pure (.letE x ty' val' body', bodyTy)

end

Synthesis handles variables, the universe, Unit, Pi, application, the annotated lambda, and let; the unannotated lambda and bare unit refuse with an error instead. That refusal is the answer to chapter 1's question: let carries an annotation so that definitions always synthesize, and lambdas may omit theirs exactly when the type arrives from outside. The refusals are also this language's honest cliff edge. Lean, given fun x => x in a vacuum, would mint a metavariable for the domain and hope to solve it later; our checker has no metavariables, and the closing section says what that costs. The contrast in the other direction is Hindley–Milner, the design that pushes everything into synthesis and buys full inference with unification over a deliberately rigid type language; bidirectional typing spends annotations to scale where that rigidity cannot, and the Dunfield–Krishnaswami survey tells the full story.

The checker speaks

Everything on this page so far is a pure function, so the game of chapter 0 repeats: pure logic first, reporting at the edge. The edge here is a pair of Lean commands that run chapter 1's parser and this chapter's checker and print the verdict into the Infoview; how such commands are built is the business of chapter 3 and chapter 4, so until then they are a black box with a visible output. One honest disappointment should be registered now: the programs can only arrive as quoted strings, with escaped backslashes and none of the editor's help, because at this point Lean knows nothing of the object language's grammar, and the only parser in the world is the one chapter 1 built. A language deserves better than being smuggled in as string data, and chapter 5 delivers better: it teaches the grammar to Lean itself, and the quotes fall away. Every output below is pinned by the build: if the checker ever disagrees with what this page shows, the site fails to compile.

open Lean Elab Command in
elab "#check_dtt " s:str : command => do
  let some raw := parseRaw s.getString
    | throwError "parse error"
  match synth Cxt.empty raw with
  | .error e => throwError e
  | .ok (tm, ty) =>
    logInfo s!"{showTm Cxt.empty tm} : {showTy Cxt.empty ty}"

open Lean Elab Command in
elab "#eval_dtt " s:str : command => do
  let some raw := parseRaw s.getString
    | throwError "parse error"
  match synth Cxt.empty raw with
  | .error e => throwError e
  | .ok (tm, ty) =>
    logInfo s!"{showTm Cxt.empty (nf [] ty tm)} : {showTy Cxt.empty ty}"

The polymorphic identity, typed and then run at a type:

/-- info: let id : (A : U) -> A -> A = \A. \x. x; id : (A : U) -> A -> A -/
#guard_msgs in
#check_dtt "let id : (A : U) -> A -> A = \\A. \\x. x; id"

/-- info: unit : Unit -/
#guard_msgs in
#eval_dtt "let id : (A : U) -> A -> A = \\A. \\x. x; id Unit unit"

An annotated lambda synthesizes its Pi; the bare one refuses, in words this chapter can now stand behind:

/-- info: \(A : U). \(x : A). x : (A : U) -> (x : A) -> A -/
#guard_msgs in
#check_dtt "\\(A : U). \\(x : A). x"

/--
error: cannot synthesize the type of an unannotated lambda; annotate the binder, or let it inherit an expected type
-/
#guard_msgs in
#check_dtt "\\x. x"

A mismatch, caught by conversion inside the mode switch:

/-- error: type mismatch: expected Unit, found U -/
#guard_msgs in
#check_dtt "let u : Unit = U; u"

And the eta laws, visible. The identity on functions into Unit normalizes to the function that ignores its argument and returns unit, because at type Unit there is nothing else to be:

/-- info: \f. \_. unit : (f : Unit -> Unit) -> Unit -> Unit -/
#guard_msgs in
#eval_dtt "\\(f : Unit -> Unit). f"

/-- info: \h. \_. unit : (h : Unit -> Unit) -> Unit -> Unit -/
#guard_msgs in
#eval_dtt "let f : (Unit -> Unit) -> Unit -> Unit = \\g. g; \
  \\(h : Unit -> Unit). f h"

A last honest word on U : U, the rule that made the universe a member of itself in synth. It keeps this chapter free of universe bookkeeping, and it makes the theory inconsistent as a logic: Girard's paradox lives in this language, although no short term exhibits it. Elaboration-zoo makes the same choice for the same reason. These lectures keep the shortcut, and chapter 4 will hold it up against Lean's own checker, which refuses it.

The cliff: metavariables

What separates this checker from Lean's elaborator is one feature: holes. Lean writes _, mints a metavariable, and solves it later from how the hole is used; our checker refuses the unannotated lambda precisely because it has nothing to mint. Adding holes is the third step of elaboration-zoo, and it reshapes the machinery this chapter built: neutrals split into those blocked on a variable and those blocked on an unsolved metavariable, and conversion generalizes from checking equalities to solving them. The solvable equations are the ones whose unknown is applied to distinct bound variables, the pattern fragment. The name has an honest etymology, best given in Miller's own words: "The unification of simply typed λ-terms modulo the rules of β- and η-conversions is often called 'higher-order' unification because of the possible presence of variables of functional type", but "in order to avoid using the very vague and over used adjective 'higher-order', we shall refer to the problem of unifying simply typed λ-terms modulo β- and η-conversion as βη-unification". The pattern fragment is the corner of that problem where unique solutions exist. Cockx's thesis surveys where the subject went from there. These lectures stop at the cliff; chapter 3 turns instead to the elaborator that already has all of it.

A road not taken: higher-order syntax

One representation decision deserves its footnote. Binders here are first-order: a closure is data, an environment and a term. Lean can express the other choice, parametric higher-order abstract syntax, where a binder is a Lean function and the metalanguage manages scope; the official PHOAS example under Further reading is exactly that. The road is not taken because this chapter needs to print, compare, and quote under binders, and each of those is awkward when binders are opaque functions. The two roads are not strangers, though: by the functional correspondence of Ager, Biernacki, Danvy, and Midtgaard, the first-order closures used here are what a higher-order evaluator becomes under defunctionalization, mechanically. Running that derivation on this chapter's evaluator is how these lectures end, in chapter 7.

Further reading

• Kovács, elaboration-zoo: projects 01 and 02 are this chapter in Haskell, and project 03 is the cliff, holes and pattern unification included. <- back
• Christiansen, Checking Dependent Types with Normalization by Evaluation: A Tutorial: the source of the explicit, type-annotated Neutral and of type-directed readback, with eta for functions, pairs, and the unit type. <- back
• Dunfield and Krishnaswami, Bidirectional Typing: the survey, including the design space this chapter walked one path of. <- back
• type theory in the nLab: the natural-deduction presentation quoted in the opening section, four kinds of rule declaring each kind of type. <- back
• Nederpelt and Geuvers, Type Theory and Formal Proof: An Introduction: a gentle, step-by-step development of derivation rules like the ones above, from the untyped lambda calculus upward. <- back
• You Could Have Invented De Bruijn Indices at the n-Category Café: the representation, reconstructed from the pain it removes. <- back
• De Bruijn index on Wikipedia: the source of the branching term drawn twice above, pictured there with one-based indices. <- back
• Miller, Unification of Simply Typed Lambda-Terms as Logic Programming: the report the prose quotes come from, with the name βη-unification. <- back
• Miller, A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification: where the pattern fragment first appears, as the Lλ subset, whose unification problems are decidable and possess most general unifiers when unifiers exist. <- back
• Cockx, Dependent Pattern Matching and Proof-Relevant Unification: the survey pointer for unification in dependent type theory. <- back
• Parametric Higher-Order Abstract Syntax from the Lean examples: the road not taken, expressible in the metalanguage we are using. <- back
• Ager, Biernacki, Danvy, and Midtgaard, A Functional Correspondence between Evaluators and Abstract Machines: closures as defunctionalized higher-order evaluation, made precise. <- back
• Kiselyov, Normalization by Evaluation in the tagless-final style: NbE with higher-order syntax, for the reader who wants to see the other road walked. <- back
• Coquand, Kinoshita, Nordström, and Takeyama, A simple type-theoretic language: Mini-TT: the entries above already cover its themes, but this one is the classic, and it reads best after the others, as the compact original so much of them descends from. <- back