|
|
|
||
Poslední úprava: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (08.12.2022)
|
|
||
Poslední úprava: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (08.12.2022)
Předmět je zakončen ústní zkouškou. |
|
||
Poslední úprava: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (08.12.2022)
Blanchette et at. The Hitchhiker's Guide to Logical Verification (available online)
Jeremy Avigad, Leonardo de Moura, and Soonho Kong. Theorem Proving in Lean (available online) |
|
||
Poslední úprava: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (08.12.2022)
Požadavky budou upřesněny. |
|
||
Poslední úprava: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (08.12.2022)
Většinou se budeme řídit textem The Hitchhiker's Guide to Logical Verification:
Základy:
(kvantifikátory, spojky, taktiky, věty jako typy / důkazy jako termy).
Funkcionálně-logické programování:
(základní datové struktury, důkazy indukcí, aritmetické taktiky).
Sémantika programů:
(small-step/big-step, částečná vs. úplná správnost, monotónní funkce, svazy a pevné body).
Matematika:
(základní principy, podtypy, kvocientové typy, třídy typů). |