Sylabus
Většinou se budeme řídit textem The Hitchhiker's Guide to Logical Verification:
Základy:
- definice a výroky,
- Backward Proofs, Forward Proofs,
(kvantifikátory, spojky, taktiky, věty jako typy / důkazy jako termy).
Funkcionálně-logické programování:
- funkcionální programování,
- induktivní predikáty,
- monády,
(základní datové struktury, důkazy indukcí, aritmetické taktiky).
Sémantika programů:
- operační sémantika,
- Hoareova logika,
- denotační sémantika,
(small-step/big-step, částečná vs. úplná správnost, monotónní funkce, svazy a pevné body).
Matematika:
- logické základy matematiky,
- základní matematické struktury,
- racionální a reálná čísla,
(základní principy, podtypy, kvocientové typy, třídy typů).
Anotace
The topic of the course are formal (computer-understandable) mathematics and proof assistants (interactive theorem provers). A proof assistent is a tool to assist with the development of formal proofs by human-machine collaboration.
The language of communication is some variant of formal logic and the main aim a high level of assurance that the proven actually holds.We will have a look at the proof assistent Lean, study its theoretical foundations and explore the ways in which it can be used to develop theories, model systems, and prove theorems in computer science.