Teaching‎ > ‎Aarhus Mini-course‎ > ‎

Day 1

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):
  • Book: 1.1—1.5, 1.7—1.8, 2.1—2.2, 2.7, 3.3, 3.5, 3.8, 4.1, 4.4, 4.5, 4.8
  • Preprint: 1.1—1.6, 2.1—2.2, 3.2, 3.4, 4.1—4.2, 4.5
Homework: In the file Homework1.agda there are some goals relating to arithmetic on binary numbers (a quite more efficient representation of numbers in proof assistants instead of the usual unary ones). Fill in those goals. Can you also show theorem-1 and theorem-2?
Č
ċ
ď
Day1.agda
(2k)
Danko Ilik,
Sep 17, 2012, 11:25 AM
ċ
ď
Homework1.agda
(2k)
Danko Ilik,
Sep 17, 2012, 11:30 AM
Comments