A tantárgy az alábbi témakörök ismeretére épít:
Bevezető analízis, matematika alapjai.
A tantárgy szerepe a képzés céljának megvalósításában:
Szabadon választható tárgy
A tantárgy részletes tematikája magyarul és angolul:
Induktív adattípusok, természetes számok, listák, fák és rekurziómentes adattípusok definiálása és manipulálása. Állítástípusok és bizonyítások definiálása és kezelése. A funkcionális programozás és a logika kapcsolata: Curry–Howard-izomorfizmus. A bizonyításkeresés automatizálása és elemi taktikák. A Coq teljes kifejezőereje: függő típusok és magasabb rendű logikák. Matematikai elméletek építése, modulok és taktikák programozása.
Követelmények szorgalmi időszakban:
A félév során két zh, és prezentáció tartása vagy projektmunka bemutatása.
Konzultációs lehetőségek:
Jegyzet, tankönyv, felhasználható irodalom:
Yves Bertot, Pierre Casteran, 2004. Interactive Theorem Proving and Program Development: Coq Art, Springer.
Nyomtatóbarát változat
