FI:I038 Types and Proofs - Course Information

I038 Types and Proofs

Faculty of Informatics
Autumn 1997

Extent and Intensity

2/0. 3 credit(s). 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

Contact Person: prof. RNDr. Jiří Zlatuška, CSc.

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

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.

Language of instruction

Czech