|
|
|
||
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (02.01.2024)
|
|
||
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (21.05.2021)
Předmět je zakončen ústní zkouškou. |
|
||
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (07.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. (21.05.2021)
Will be specified later. |
|
||
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (01.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) |