2400097 – Constructive Logic

This course provides a thorough introduction to modern constructive logic, emphasizing its numerous applications in computer science, and its mathematical properties. The core topics of this course are intuitionistic logic, natural deduction, Curry-Howard isomorphism, propositions as types, proofs as programs, formulas as programs, constructive logic as functional programming, constructive logic as logic programming, Heyting arithmetic induction as primitive recursion, cut elimination, sequent calculus, contraction-free proofs, inversion, and decidable fragments. Advanced topics may include type theory, proof search, linear logic, temporal logic, intuitionistic modal logic.