IA038 Types and Proofs

Faculty of Informatics
Spring 2018
Extent and Intensity
2/0. 3 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. Mojmír Křetínský, 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
Tue 13:00–14:50 B515
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 19 fields of study the course is directly associated with, display
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
Study Materials
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 2021, Spring 2023, Autumn 2024.
  • Enrolment Statistics (Spring 2018, recent)
  • Permalink: https://is.muni.cz/course/fi/spring2018/IA038