IA038 Types and Proofs

Faculty of Informatics
Spring 2011
Extent and Intensity
2/0. 3 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Alternate Types of Completion: k (colloquium), z (credit).
Teacher(s)
prof. RNDr. Jiří Zlatuška, CSc. (lecturer)
Supervisor
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science - Faculty of Informatics
Contact Person: prof. RNDr. Jiří Zlatuška, CSc.
Timetable
Mon 10:00–11:50 B204
Course Enrollment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
Fields of study the course is directly associated with
there are 18 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
  • GIRARD, Jean-Yves, Paul TAYLOR and Yves LAFONT. Proofs and types. Cambridge: Cambridge University Press, 1989. xi, 176 s. ISBN 0-521-37181-3. info
  • ZLATUŠKA, Jiří. Lambda-kalkul. Vyd. 1. Brno: Masarykova univerzita, 1993. 264 s. ISBN 80-210-0826-1. info
Further Comments
Study Materials
The course is also listed under the following terms Spring 2003, Spring 2006, Spring 2013.
  • Enrollment Statistics (Spring 2011, recent)
  • Permalink: https://is.muni.cz/course/fi/spring2011/IA038

Other references: 

Go to top | Current date and time: 23. 5. 2013 06:55, Week 21 (odd)

Contact: istech(zavináč/atsign)fi(tečka/dot)muni(tečka/dot)cz, Office for Studies, access rights administrators, is-technicians, e-technicians, IT support | learn more about Information System