|
|
|
||
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (08.12.2022)
|
|
||
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (08.12.2022)
Předmět je zakončen ústní zkouškou. |
|
||
Last update: 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) |
|
||
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (08.12.2022)
Will be specified later. |
|
||
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (08.12.2022)
We will mostly follow the Hitchhiker's Guide:
Basics:
(Quantifiers, Connectives, Tactics, Propositions as Types / Proofs as Terms)
Functional–Logic Programming:
(Basic Data Structures, Proofs by induction, Arithmetic tactics)
Program Semantics:
(Small-step/big-step, Partial vs Total correctness, Monotone functions, lattices and fixpoints)
Mathematics:
(Foundational principles, Subtypes, Quotient types, Type Classes) |