Typové systémy

Předmět není vypsán Nerozvrhuje se

Kód	Zakončení	Kredity	Rozsah	Jazyk výuky
A7B36TYS	Z,ZK	5	2+2s	česky

Přednášející:

Cvičící:

Předmět zajišťuje:

katedra počítačů

Anotace:

V tomto předmětu se studenti naučí specifikovat typové systémy reálných programovacích jazyků, analyzovat jejich vlastnosti a dokazovat jejich korektnost.

Požadavky:

znalost programování, znalost funkcionálního programování výhodou

Osnova přednášek:

Smysl typových systémů

Netypované aritmetické výrazy

Netypovaný lambda kalkulus

Typované aritmetické výrazy

Jednoduše typovaný lambda kalkulus

Jednoduchá rozšíření

Normalizace

Reference

Výjimky

Podtypy

Metateorie podtypování

Případová studie: imperativní objekty

Případová studie: Featherweight Java

Osnova cvičení:

Smysl typových systémů

Netypované aritmetické výrazy

Netypovaný lambda kalkulus

Typované aritmetické výrazy

Jednoduše typovaný lambda kalkulus

Jednoduchá rozšíření

Normalizace

Reference

Výjimky

Podtypy

Metateorie podtypování

Případová studie: imperativní objekty

Případová studie: Featherweight Java

Cíle studia:

Studijní materiály:

B. Pierce: Types and Programming Languages

Poznámka:

Další informace:

Pro tento předmět se rozvrh nepřipravuje

Předmět je součástí následujících studijních plánů: