IA038 Types and Proofs

Faculty of Informatics
Spring 2021
Extent and Intensity
2/0. 2 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium), z (credit).
Teacher(s)
prof. RNDr. Jiří Zlatuška, CSc. (lecturer)
Guaranteed by
prof. RNDr. Jiří Zlatuška, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: prof. RNDr. Jiří Zlatuška, CSc.
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Mon 10:00–11:50 Virtuální místnost
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
Course objectives
This course delivers focuses on the correspondence between proof theory and typed lambda-calculus and its generalization to the correspondence between computations as proof simplifications and program specifications as types in various formal settings. The contents of the course is relevant for work in many areas of theoretical computer science.
Syllabus
  • Meaning and denotation in logic, tarski and Heyting.
  • natural deduction: calculus, rules, computational interpretation.
  • Curry-Howard isomorphism: lambda-calculus, operational and denotational interpretation, conversion, isomorphism.
  • Normalization theorem: Church-Rosser property, weak normalization, strong normalization.
  • Sequent calculus: structural rules, intuitionistic version, identities, logical rules, properties of the cut-free system, translation between sequent calculus and natural deduction.
  • Strong normalization theorem: reducibility and its properties.
  • Gödels system T, calculus, normalization, expressive power.
  • Coherent spaces, stabil functions, paralel disjunction, product and function spaces, denotational semantics of System T.
  • Sums in natural deduction: problems, standard conversion, commuting conversions, functional calculus.
  • System F: calculus, simple types, free structures, inductive types, Curry-Howard isomorphism, strong normalization.
  • Coherent semantics of the sum; cut-elimination theorem; representation.
Literature
  • ZLATUŠKA, Jiří. Lambda-kalkul. 1. vyd. Brno: Masarykova univerzita, 1993, 264 s. ISBN 8021008261. info
  • GIRARD, Jean-Yves, Paul TAYLOR and Yves LAFONT. Proofs and types. Cambridge: Cambridge University Press, 1990, xi, 176. ISBN 0521371813. info
Language of instruction
Czech
Further Comments
The course is taught once in two years.
The course is also listed under the following terms Spring 2003, Spring 2006, Spring 2011, Spring 2013, Spring 2016, Spring 2018, Spring 2023, Autumn 2024.
  • Enrolment Statistics (Spring 2021, recent)
  • Permalink: https://is.muni.cz/course/fi/spring2021/IA038