Přednášky Anstena Kleva

Constructive Type Theory

Ansten Klev

8. 10. 2015, 10:00, Zasedací místnost FLÚ

General introduction; the notions of judgement and proposition; the notions of type and set; the hierarchy of higher types.

15. 10. 2015, 14:00, Zasedací místnost CMS

The Curry-Howard isomorphism; formation-, introduction-, elimination-, and identity-rules; the logical constants.

22. 10. 2015, 14:00, Zasedací místnost ÚDU

More constants: the natural numbers, finite sets, propositional identity.

Abstrakt kurzu