FI:IA038 Types and Proofs - Informace o předmětu

IA038 Types and Proofs

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

• Analýza a zpracování obrazu (program FI, N-VIZ)
• Bioinformatika a systémová biologie (program FI, N-UIZD)
• Computer Games Development (program FI, N-VIZ_A)
• Computer Graphics and Visualisation (program FI, N-VIZ_A)
• Computer Networks and Communications (program FI, N-PSKB_A)
• Cybersecurity Management (program FI, N-RSSS_A)
• Diskrétní algoritmy a modely (program FI, N-TEI)
• Formální analýza počítačových systémů (program FI, N-TEI)
• Grafický design (program FI, N-VIZ)
• Graphic Design (program FI, N-VIZ_A)
• Hardware Systems (program FI, N-PSKB_A)
• Hardwarové systémy (program FI, N-PSKB)
• Image Processing and Analysis (program FI, N-VIZ_A)
• Informační bezpečnost (program FI, N-PSKB)
• Information Security (program FI, N-PSKB_A)
• Kvantové a jiné neklasické výpočetní modely (program FI, N-TEI)
• Počítačová grafika a vizualizace (program FI, N-VIZ)
• Počítačové sítě a komunikace (program FI, N-PSKB)
• Principy programovacích jazyků (program FI, N-TEI)
• Řízení kyberbezpečnosti (program FI, N-RSSS)
• Řízení vývoje služeb (program FI, N-RSSS)
• Řízení vývoje softwarových systémů (program FI, N-RSSS)
• Services Development Management (program FI, N-RSSS_A)
• Software Systems Development Management (program FI, N-RSSS_A)
• Softwarové systémy (program FI, N-PSKB)
• Strojové učení a umělá inteligence (program FI, N-UIZD)
• Vývoj počítačových her (program FI, N-VIZ)
• Zpracování a analýza rozsáhlých dat (program FI, N-UIZD)
• Zpracování přirozeného jazyka (program FI, N-UIZD)

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

• Statistika zápisu (nejnovější)
  
• Permalink: https://is.muni.cz/predmet/fi/podzim2024/IA038