FI:IA038 Types and Proofs - Course Information

IA038 Types and Proofs

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

• Image Processing and Analysis (programme FI, N-VIZ)
• Bioinformatics and systems biology (programme FI, N-UIZD)
• Computer Games Development (programme FI, N-VIZ_A)
• Computer Graphics and Visualisation (programme FI, N-VIZ_A)
• Computer Networks and Communications (programme FI, N-PSKB_A)
• Cybersecurity Management (programme FI, N-RSSS_A)
• Discrete algorithms and models (programme FI, N-TEI)
• Formal analysis of computer systems (programme FI, N-TEI)
• Graphic design (programme FI, N-VIZ)
• Graphic Design (programme FI, N-VIZ_A)
• Hardware Systems (programme FI, N-PSKB_A)
• Hardware systems (programme FI, N-PSKB)
• Image Processing and Analysis (programme FI, N-VIZ_A)
• Information security (programme FI, N-PSKB)
• Information Security (programme FI, N-PSKB_A)
• Quantum and Other Nonclassical Computational Models (programme FI, N-TEI)
• Computer graphics and visualisation (programme FI, N-VIZ)
• Computer Networks and Communications (programme FI, N-PSKB)
• Principles of programming languages (programme FI, N-TEI)
• Cybersecurity management (programme FI, N-RSSS)
• Services development management (programme FI, N-RSSS)
• Software Systems Development Management (programme FI, N-RSSS)
• Services Development Management (programme FI, N-RSSS_A)
• Software Systems Development Management (programme FI, N-RSSS_A)
• Software systems (programme FI, N-PSKB)
• Machine learning and artificial intelligence (programme FI, N-UIZD)
• Computer Games Development (programme FI, N-VIZ)
• Processing and analysis of large-scale data (programme FI, N-UIZD)
• Natural language processing (programme FI, N-UIZD)

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