Teória typov

Informácie o predmete

O predmete

Typový systém priraďuje výrazom programu typy podľa formálnych pravidiel. Umožňuje tak odhaliť určité chyby ešte pred vykonaním programu a uvažovať o jeho vlastnostiach. Teória typov poskytuje základy pre návrh programovacích jazykov, typovú kontrolu aj konštrukciu dôkazov.

Na predmete budeme skúmať syntax, operačnú sémantiku a typovanie programovacích jazykov. Východiskom bude λ-kalkul a jazyk čísel a pravdivostných hodnôt NBL. Výklad rozšírime o polymorfizmus, závislé typy a súvislosti medzi typmi, programami a logickými dôkazmi. Vybrané definície a vlastnosti budeme formalizovať v interaktívnom dokazovacom systéme Rocq.

Ciele predmetu

Cieľom predmetu je:

  • vysvetliť princípy typových systémov a ich úlohu pri návrhu programovacích jazykov;
  • analyzovať a vyhodnocovať termy netypovaného a jednoducho typovaného λ-kalkulu;
  • používať pravidlá operačnej sémantiky a konštruovať typové odvodenia;
  • dokazovať základné vlastnosti typových systémov, najmä progres a zachovanie typu;
  • formalizovať definície a tvrdenia v Rocqu a konštruovať ich dôkazy pomocou taktík.

Študijné materiály a nástroje

Materiály sú dostupné v navigácii predmetu:

  • Prednášky vysvetľujú pojmy, formálne pravidlá a vlastnosti typových systémov na riešených príkladoch.
  • Cvičenia obsahujú úlohy na vyhodnocovanie termov, typovanie a odvodenie typov.
  • Interaktívny dokazovací systém Rocq Prover obsahuje materiály k definíciám údajových typov a funkcií, logickým tvrdeniam a dôkazovým taktikám. Súčasťou sú formálne dôkazy overované v systéme Rocq.

Rocq Game – precvičovanie dôkazov v prehliadači

Vzdelávacia aplikácia vyvíjaná na Technickej univerzite v Košiciach umožňuje precvičovať definície a dôkazové taktiky na úlohách usporiadaných do tematických svetov a úrovní. Dôkazy overuje Rocq priamo vo webovom prehliadači, bez potreby lokálnej inštalácie.

Obsah predmetu

Osnova podľa informačného listu predmetu:

  1. Základné pojmy teórie typov.
  2. Netypovaný jazyk čísel a pravdivostných hodnôt, NBL.
  3. Netypovaný λ-kalkul.
  4. Typovaný NBL.
  5. Jednoducho typovaný lambda kalkul.
  6. Odvodené tvary termov.
  7. Súčinové a súčtové typy.
  8. Rekurzia a rekurzívne typy.
  9. Závislé typy.
  10. Polymorfné typy.
  11. Typová rekonštrukcia – odvodenie typu.
  12. Systém F, Let polymorfizmus.

Hodnotenie predmetu

  • Zápočet: maximálne 40 bodov, potrebné minimum je 21 bodov.
  • Skúška: maximálne 60 bodov, potrebné minimum je 31 bodov.

Podrobné podmienky hodnotenia sú zverejnené v kurze predmetu v systéme Moodle.

Vyučujúci

Prednášky a cvičenia vedie Ing. Ján Perháč, PhD.. Kontakt: jan.perhac@tuke.sk.

Poďakovanie

Ministerstvo školstva, výskumu, vývoja a mládeže Slovenskej republiky

Aktualizácia a rozvoj študijných materiálov pre predmet Teória typov sú podporené Kultúrnou a edukačnou grantovou agentúrou (KEGA) Ministerstva školstva, výskumu, vývoja a mládeže Slovenskej republiky v rámci projektu 052TUKE-4/2025 – Moderné prístupy vo vzdelávaní IT odborníkov v oblasti Teórie typov.

Informácie o projekte na Portáli VŠ

Odporúčaná literatúra

  1. B. C. Pierce. Types and Programming Languages. MIT Press, Cambridge, 2002.
    Перевод на русский язык: Бенджамин Пирс. Типы в языках программирования. Добросвет, 2012. 680 с. ISBN 978-5-7913-0082-9.
  2. B. C. Pierce a kol. Software Foundations. Elektronická učebnica, 2024.
  3. V. Novitzká, D. Mihályi. Teória typov. Technická univerzita v Košiciach, 2015.
  4. J.-Y. Girard. Proofs and Types. Cambridge University Press, 1989.
  5. J. R. Hindley. Basic Simple Type Theory. Cambridge University Press, 1997.
  6. R. Sethi. Programming Languages: Concepts and Constructs. Addison-Wesley, 1996.
  7. W. Horowitz. Higher-order Programming Languages. Wiley & Sons, 1982.
  8. Computer Science Center. Введение. Функциональное и императивное программирование. 2015. Prednášky sú dostupné v playliste na YouTube.
© Copyright 2026 KPI FEI TUKE