FI:IA038 Types and Proofs - Course Information

IA038 Types and Proofs

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

Mon 10:00–11:50 B411

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

• Applied Informatics (programme FI, N-AP)
• Information Technology Security (eng.) (programme FI, N-IN)
• Information Technology Security (programme FI, N-IN)
• Bioinformatics (programme FI, N-AP)
• Information Systems (programme FI, N-IN)
• Parallel and Distributed Systems (programme FI, N-IN)
• Computer Graphics (programme FI, N-IN)
• Computer Networks and Communication (programme FI, N-IN)
• Computer Systems (programme FI, N-IN)
• Embedded Systems (eng.) (programme FI, N-IN)
• Embedded Systems (programme FI, N-IN)
• Service Science, Management and Engineering (eng.) (programme FI, N-AP)
• Service Science, Management and Engineering (programme FI, N-AP)
• Social Informatics (programme FI, B-AP)
• Theoretical Informatics (programme FI, N-IN)
• Upper Secondary School Teacher Training in Informatics (programme FI, N-SS) (2)
• Artificial Intelligence and Natural Language Processing (programme FI, N-IN)
• Image Processing (programme FI, N-AP)

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 annually.

• Enrolment Statistics (Spring 2016, recent)
  
• Permalink: https://is.muni.cz/course/fi/spring2016/IA038