IA038 Types and Proofs

Faculty of Informatics
Autumn 2024
Extent and Intensity
2/0/0. 2 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium), z (credit).
In-person direct teaching
Teacher(s)
Dr. rer. nat. Achim Blumensath (lecturer)
Guaranteed by
Dr. rer. nat. Achim Blumensath
Department of Computer Science – Faculty of Informatics
Contact Person: Dr. rer. nat. Achim Blumensath
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Thu 26. 9. to Thu 21. 11. Thu 12:00–13:50 C511, Thu 28. 11. to Thu 19. 12. Thu 12:00–13:50 S209
Prerequisites
The course assumes some familiarity with first-order logic. Knowledge of lambda-calculus is useful, but not required.
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
fields of study / plans the course is directly associated with
there are 29 fields of study the course is directly associated with, display
Course objectives
This is a theoretical course examining a correspondence between type systems and certain logic calculi. It can be seen as a companion to the course IA011 Programming Language Semantics. The target audience are students with an interest in proof calculi and the lambda-calculus.
Learning outcomes
After completing the course, students will understand the basic properties of intuitionistic logic. They will be able to compare proof calculi with typed versions of the lambda-calculus, and to transfer programming language constructs into logic and vice versa.
Syllabus
  • intuitionistic logic
  • the simply typed lambda-calculus
  • the Howard-Curry correspondence
  • combinators
  • classical logic
  • first-order logic
  • second-order logic
  • dependent types
Literature
    recommended literature
  • SØRENSEN, Morten Heine B. and Pawel URZYCZYN. Lectures on the Curry-Howard isomorphism. 1st ed. Amsterdam: Elsevier, 2006, xiv, 442. ISBN 0444520775. info
  • GIRARD, Jean-Yves, Paul TAYLOR and Yves LAFONT. Proofs and types. Cambridge: Cambridge University Press, 1990, xi, 176. ISBN 0521371813. info
Teaching methods
lectures
Assessment methods
written exam
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
The course is also listed under the following terms Spring 2003, Spring 2006, Spring 2011, Spring 2013, Spring 2016, Spring 2018, Spring 2021, Spring 2023.
  • Enrolment Statistics (recent)
  • Permalink: https://is.muni.cz/course/fi/autumn2024/IA038