xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
Interactive and Automated Proving of Program Correctness
| Type of study | Follow-up Master |
|---|---|
| Language of instruction | English |
| Code | 460-4145/02 |
| Abbreviation | IADKP |
| Course title | Interactive and Automated Proving of Program Correctness |
| Credits | 4 |
| Coordinating department | Department of Computer Science |
| Course coordinator | doc. Ing. Zdeněk Sawa, Ph.D. |
Subject syllabus
E-learning
Materials are available on the educator's website: https://www.cs.vsb.cz/sawa/iadkp
Consultation through MS Teams.
Consultation through MS Teams.
Literature
[1] Benjamin C. Pierce et al. - Software Foundations (volumes 1 - 5). Electronic textbook, version 5.8., 2020. Dostupné na adrese https://softwarefoundations.cis.upenn.edu
Advised literature
[2] Yves Bertot, Pierre Castéran - Interactive Theorem Proving and Program Development, Springer, 2004.
[3] Andrew W. Appel et al. - Program Logics for Certified Compilers, Cambridge University Press, 2014.
[4] Adam Chlipala - Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press, 2013.
[5] Benjamin C. Pierce - Types and Programming Languages, MIT Press, 2002.
[6] Benjamin C. Pierce, ed. - Advanced Topics in Types and Programming Languages. MIT Press, 2004.
[7] Glynn Winskel - Formal Semantics of Programming Languages, The MIT Press, 1993.
[8] Hans Hüttel - Transitions and Trees: An Introduction to Structural Operational Semantics, Cambridge University Press, 2010.
[3] Andrew W. Appel et al. - Program Logics for Certified Compilers, Cambridge University Press, 2014.
[4] Adam Chlipala - Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press, 2013.
[5] Benjamin C. Pierce - Types and Programming Languages, MIT Press, 2002.
[6] Benjamin C. Pierce, ed. - Advanced Topics in Types and Programming Languages. MIT Press, 2004.
[7] Glynn Winskel - Formal Semantics of Programming Languages, The MIT Press, 1993.
[8] Hans Hüttel - Transitions and Trees: An Introduction to Structural Operational Semantics, Cambridge University Press, 2010.