Computation Theory · Cluster
Proof and Types
Curry-Howard, proof assistants, and typed computation.
- 01 Natural Deduction: Why Implication Is Defined by Two Rules How introduction and elimination rules fix the meaning of implication, why the pair must be in harmony, and what a local reduction step removes from a derivation.
- 02 Proof Terms: Reading a Derivation as a Program The correspondence between natural-deduction proofs and typed lambda terms, why normalisation is evaluation, and which logical principles correspond to which programming constructs.
- 03 The Sequent Calculus and Why Its Rules Are Invertible How Gentzen's sequent presentation differs from natural deduction, why left and right rules can be read backwards for proof search, and what the cut rule adds.
- 04 Cut Elimination and the Subformula Property Why removing the cut rule from a derivation bounds proof search to subformulas of the goal, what the elimination procedure costs, and where the bound fails to be useful.
- 05 Dependent Types: Pi and Sigma as Generalised Function and Pair How quantifying over a type lets the result type mention the argument, why checking such types needs conversion, and where the dependent eliminators differ from the simply typed ones.
- 06 Definitional and Propositional Equality Why a type checker can only decide equality by computation, what must be proved as a proposition instead, and how equality reflection changes the boundary between the two.
- 07 Normalisation by Evaluation for Conversion Checking How to decide equality of terms by evaluating them into a semantic domain of closures and neutral values, and why this avoids the quadratic cost of substitution.
- 08 Elaboration: Filling in What the Program Did Not Say How metavariables, unification, and implicit arguments turn surface syntax into a fully explicit core term, and why the process can fail in ways the source does not explain.
- 09 The De Bruijn Criterion and What a Proof Kernel May Assume Why a proof assistant separates a small trusted checker from large automation, what the kernel must implement, and which shortcuts quietly enlarge what must be trusted.
- 10 Termination Checking and the Price of Consistency Why a total language cannot have a general fixpoint, how structural and size-change checks approximate termination, and what each approximation rejects.