IA038 Types and Proofs

Fakulta informatiky
podzim 2024
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
Čt 26. 9. až Čt 21. 11. Čt 12:00–13:50 C511, Čt 28. 11. až Čt 19. 12. Čt 12:00–13:50 S209
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
Cíle předmětu
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.
Osnova
  • intuitionistic logic
  • the simply typed lambda-calculus
  • the Howard-Curry correspondence
  • combinators
  • classical logic
  • first-order logic
  • second-order logic
  • dependent types
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
Výukové metody
lectures
Metody hodnocení
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.
  • Statistika zápisu (nejnovější)
  • Permalink: https://is.muni.cz/predmet/fi/podzim2024/IA038