INFORMAČNÝ LIST PREDMETU
Vysoká škola: Technická univerzita v Košiciach
Fakulta: Fakulta elektrotechniky a informatiky
Pracovisko: Katedra počítačov a informatiky
Kód predmetu: 2616071 Názov predmetu: Teória typov
Druh, rozsah a metóda vzdelávacích činností:
Forma výučby: Prednáška, Cvičenie numerické
Odporúčaný rozsah výučby (v hodinách):
Denná forma štúdia (hodiny za týždeň): 2,2
Externá forma štúdia (hodiny za semester): 26,26
Metóda štúdia:
Počet kreditov: 6
Odporúčaný semester štúdia: ZS
Odporúčaný semester Študijný program Stupeň štúdia Metóda štúdia
1.rok ZS Kyberbezpečnosť (KB_Ing_D_sk)
Informatika (INF_Ing_D_sk)
Počítačové modelovanie (PM_Ing_D_sk)
Informatika (INF_Ing_D_en)
2.
2.
2.
2.
Prezenčná
Prezenčná
Prezenčná
Prezenčná
2.rok ZS Kyberbezpečnosť (KB_Ing_D_sk)
Informatika (INF_Ing_D_sk)
Informatika (INF_Ing_D_en)
2.
2.
2.
Prezenčná
Prezenčná
Prezenčná
Stupeň štúdia:
Podmieňujúce predmety:
Podmienky na absolvovanie predmetu:
Spôsob hodnotenia a skončenia štúdia predmetu: Zápočet a skúška
Priebežné hodnotenie (PH): Študent prospeje v PH a získa zápočet, keď splní podmienku získať min. 16% z 30%.
priebežné testy
Záverečné hodnotenie (ZH): Študent prospeje v ZH a úspešne vykoná skúšku, keď splní podmienku získať min. 36% z 70%.
skúška
Celkové hodnotenie: CH je suma hodnotení získaných študentom za hodnotené obdobie. Celkový výsledok sa stanoví v súlade s vnútornými predpismi TUKE. (študijný poriadok, vnútorný predpis zásady doktorandského štúdia)
Výsledky vzdelávania:
Absolvovaním predmetu získajú študenti najdôležitejšie poznatky z teórie typov. Osvoja si metódy popisu a konštrukcie základných, jednoduchých, polymorfných a závislých typov. Porozumejú rôznym prístupom a definovaniu vzťahov medzi nimi. Oboznámia sa so špeciálnymi typmi, ako sú rekurzívne a existenčné typy. Pochopia vzťah medzi typmi a formálnymi logickými systémami na báze Curry-Howardovho izomorfizmu. Na príkladoch vo funkcionálnych a procedurálnych jazykoch si precvičia použitie jednotlivých prístupov.
Stručná osnova predmetu:
1. Základné pojmy teórie typov.
2. Netypovaný jazyk čísel a pravdivostných hodnôt, NBL.
3. Netypovaný lambda 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. Referenčné typy.
10. Výnimočné situácie.
11. Podtypy.
12. Polymorfné typy.
Odporúčaná literatúra:
1. B.C.Pierce: Types and programming languages, MIT Press,  Cambridge, 2001
2. J.-Y. Girard: Proofs and types, Cambridge Univ.Press, 1989
3. J.R.Hindley: Basic simple type theory, Cambridge Univ.Press, 1997
4. R.Sethi: Programming Languages, WileyaSons, 1996
5. W.Horowitz: Higher-order Programming Languages, WileyaSons, 1982
6. Valerie Novitzká, Daniel Mihályi: Teória typov, TU Košice, 2015
Odporúčané voliteľné súčasti programu:
Jazyk, ktorého znalosť je potrebná na absolvovanie predmetu:
Poznámky:
Hodnotenie predmetov:
Celkový počet hodnotených študentov: 950
  A B C D E FX  
  39% 25% 20% 12% 2% 2%  
Zabezpečuje:
prof. RNDr. Valerie Novitzká, PhD.
doc. Ing. William Steingartner, PhD.
Ing. Ján Perháč, PhD.
Dátum poslednej zmeny: 01.09.2022
Schválil: osoba/osoby zodpovedné za študijný program