Program = Proof

This course provides a first introduction to the Curry-Howard correspondence between programs and proofs, from a theoretical programmer's perspective: we want to understand the theory behind logic and programming languages, but also to write concrete programs (in OCaml) and proofs (in Agda). After an introduction to functional programming languages, we present propositional logic, λ-calculus, the Curry-Howard correspondence, first-order logic, Agda, dependent types and homotopy type theory. Introduction Proving instead of testing Typing as proving Checking programs Checking proofs Searching for proofs Foundations In this course Other references on programs and proofs About this document Typed functional programming Introduction Hello world Execution A statically typed language A functional language Other features Basic constructions Declarations Functions Booleans Products Lists Strings Unit Recursive types Trees Usual recursive types Abstract description Option types and exceptions The typing system Usefulness of typing Properties of typing Safety Typing as proving Arrow as implication Other connectives Limitations of the correspondence Propositional logic Introduction From provability to proofs Intuitionism Formalizing proofs Properties of the logical system Natural deduction Formulas Sequents Inference rules Intuitionistic natural deduction Proofs Fragments Admissible rules Definable connectives Equivalence Structural rules Substitution Cut elimination Cuts Proof substitution Cut elimination Consistency Intuitionism Commutative cuts Proof search Reversible rules Proof search Classical logic Axioms for classical logic The intuition behind classical logic A variant of natural deduction Cut-elimination in classical logic De Morgan laws Boolean models DPLL Resolution Double-negation translation Intermediate logics Sequent calculus Sequents Rules Intuitionistic rules Cut elimination Proof search Hilbert calculus Proofs Other connectives Relationship with natural deduction Kripke semantics Kripke structures Completeness Pure lambda-calculus lambda-terms Definition Bound and free variables Renaming and alpha-equivalence Substitution beta-reduction Definition An example Reduction and redexes Confluence beta-reduction paths Normalization beta-equivalence eta-equivalence Computing in the lambda-calculus Identity Booleans Pairs Natural numbers Fixpoints Turing completeness Self-interpreting Adding constructors Confluence of the lambda-calculus Confluence The parallel beta-reduction Properties of the parallel beta-reduction Confluence and the Church-Rosser theorem Implementing reduction Reduction strategies Normalization by evaluation Nameless syntaxes The Barendregt convention De Bruijn indices Combinatory logic Simply typed lambda-calculus Typing Types Contexts lambda-terms Typing Basic properties of the typing system Type checking, type inference and typability The Curry-Howard correspondence Subject reduction eta-expansion Confluence Strong normalization A normalization strategy Strong normalization First consequences Deciding convertibility Weak normalization Other connectives Products Unit Coproducts Empty type Commuting conversions Natural numbers Strong normalization Curry style typing A typing system Principal types Computing the principal type Hindley-Milner type inference Bidirectional type checking Hilbert calculus and combinators Classical logic Felleisen's C The lambdamu-calculus Classical logic as a typing system A more symmetric calculus First-order logic Definition Signature Terms Substitutions Formulas Bound and free variables Natural deduction rules Classical first order logic Sequent calculus rules Cut elimination Eigenvariables Curry-Howard Theories Equality Properties of theories Models Presburger arithmetic Peano and Heyting arithmetic Set theory Naive set theory Zermelo-Fraenkel set theory Intuitionistic set theory Unification Equation systems Most general unifier The unification algorithm Implementation Efficient implementation Resolution Agda What is Agda? Features of proof assistants Installation Getting started with Agda Getting help Shortcuts The standard library Hello world Our first proof Our first proof, step by step Our first proof, again Basic agda The type of types Arrow types Functions Postulates Records Modules Inductive types: data Natural numbers Pattern matching The induction principle Booleans Lists Options Vectors Finite sets Inductive types: logic Implication Product Unit type Empty type Negation Coproduct Pi-types Sigma-types Predicates Equality Equality and pattern matching Main properties Half of even numbers Reasoning Definitional equality More properties with equality The J rule Decidable equality Heterogeneous equality Proving programs in practice Extrinsic vs intrinsic proofs Insertion sort The importance of the specification Termination Termination and consistency Structural recursion A bit of computability The number of bits The fuel technique Well-founded induction Division and modulo Formalization of important results Safety of a simple language Natural deduction Pure lambda-calculus Naive approach De Bruijn indices Keeping track of free variables Normalization by evaluation Confluence Combinatory logic Simply typed lambda-calculus Definition Strong normalization Normalization by evaluation Dependent type theory Core dependent type theory Expressions Free variables and substitution Contexts Definitional equality Sequents Rules for contexts Rules for equality Axiom rule Terms and rules for type constructors Rules for Pi-types Admissible rules Universes The type of Type Russell's paradox in type theory Girard's paradox The hierarchy of universes More type constructors Empty type Unit type Products Dependent sums Coproducts Booleans Natural numbers Other type constructors Inductive types W-types Rules for W-types More inductive types The positivity condition Disjointedness and injectivity of constructors Implementing type theory Expressions Evaluation Convertibility Typechecking Testing Homotopy type theory Identity types Definitional and propositional equality Propositional equality in Agda The rules Leibniz equality Extensionality of equality Uniqueness of identity proofs Types as spaces Intuition about the model The structure of paths n-types Propositions Sets n-types Propositional truncation Univalence Operations with paths Equivalences Univalence Applications of univalence Describing identity types Describing propositions Incompatibility with set theoretic interpretation Equivalences Function extensionality Propositional extensionality Higher inductive types Rules for higher types Paths over Circle as a higher inductive type Useful higher inductive types Appendix Relations Definition Closure Quotient Congruence Monoids Definition Free monoids Well-founded orders Partial orders Well-founded orders Lexicographic order Trees Multisets Cantor's diagonal argument A general Cantor argument Agda formalization