Hilbert's Proof Theory: Decidablity problem, Turing's machines and Church's (untyped) lambda calculus as a response; the Church-Turing Thesis. Brouwer's Intuitionisim: recovering the original meaning of disjunction and existential quantification, the BHK "interpretation and Kleene's and Kreisel's realizability interpretations; Heting's formalization, Natural deduction system for intuitionistic logic. The Curry-Howard correspondence for intuitionistic logic and simply typed lambda calculus with pairs and sums. Proof assistants based on dependent types. Agda tutorial. Material from the Book (Preprint):
|