IA038 Types and Proofs

Fakulta informatiky
podzim 2025
Rozsah
2/0/0. 2 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k, z.
Vyučováno kontaktně
Vyučující
Dr. rer. nat. Achim Blumensath (přednášející)
Garance
Dr. rer. nat. Achim Blumensath
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: Dr. rer. nat. Achim Blumensath
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Po 15. 9. až Po 15. 12. Po 18:00–19:50 C123
Předpoklady
The course assumes some familiarity with first-order logic. Knowledge of lambda-calculus is useful, but not required.
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 29 mateřských oborů, zobrazit
Anotace
This is a theoretical course examining a correspondence between type systems and certain logic calculi. It can be seen as a companion to the course IA011 Programming Language Semantics. The target audience are students with an interest in proof calculi and the lambda-calculus.
Výstupy z učení
After completing the course, students will understand the basic properties of intuitionistic logic. They will be able to compare proof calculi with typed versions of the lambda-calculus, and to transfer programming language constructs into logic and vice versa.
Klíčová témata
  • intuitionistic logic
  • the simply typed lambda-calculus
  • the Howard-Curry correspondence
  • combinators
  • classical logic
  • first-order logic
  • second-order logic
  • dependent types
Studijní zdroje a literatura
    doporučená literatura
  • SØRENSEN, Morten Heine B. a Pawel URZYCZYN. Lectures on the Curry-Howard isomorphism. 1st ed. Amsterdam: Elsevier, 2006, xiv, 442. ISBN 0444520775. info
  • GIRARD, Jean-Yves; Paul TAYLOR a Yves LAFONT. Proofs and types. Cambridge: Cambridge University Press, 1990, xi, 176. ISBN 0521371813. info
Přístupy, postupy a metody používané ve výuce
lectures
Způsob ověření výstupů z učení a požadavky na ukončení
written exam
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2003, jaro 2006, jaro 2011, jaro 2013, jaro 2016, jaro 2018, jaro 2021, jaro 2023, podzim 2024.
  • Statistika zápisu (nejnovější)
  • Permalink: https://is.muni.cz/predmet/fi/podzim2025/IA038