FI:IA038 Types and Proofs - Course Information
IA038 Types and Proofs
Faculty of InformaticsAutumn 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 19. 9. to Thu 12. 12. Thu 12:00–13:50 C511
- 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.
- Enrolment Statistics (recent)
- Permalink: https://is.muni.cz/course/fi/autumn2024/IA038