Skip to content

Modeling and Verifying Algorithms In Coq

Public syllabus for 2025-2026

Back to syllabi

Academic overview

Programme
AIDC
Period
Year 1, Semester 2
Credits
6
Weeks
14

Curriculum placement

Appears in study plans

AIDC (2025 - 2027) Year 1, Semester 2 Elective subject, group 3

Teaching team

Course coordinator
(none)
Seminar coordinators
(none)

Learning time distribution

Total
Curriculum Lecture Practice Total Weekly Lecture Practice
42 28 14 3 2 1
Exam hours
0
Individual Study Bibliography study Field study Homework Tutoring Others
108 42 8 52 6 0
Overall
150

Learning outcomes

Knowledge

  • To understand and interact with the Coq prover / Capacitatea de intelegere si de interactiune cu demonstratorul Coq
  • To formalize in Coq data structures and their operations / Capacitatea de formalizare in Coq a structurilor de date si a operatiilor asupra lor
  • To formalize properties about these data structures and operations / Capacitatea de a formaliza proprietati despre aceste structuri de date si operatii
  • To prove these properties / Capacitatea de a demonstra aceste proprietati

Skills

  • To communicate knowledge related to formal calculus used in various activity fields/ Capacitatea de a comunica cunostinte referitore la calculul formal utilizat in diferite domenii de activitate

Responsibility

(none)

Online platform

_______________

Course content

Content Methods Obs
C1. (3h) General Introduction. Programming with natural numbers and lists in Coq (Oc, Oab, Oat) / Introducere generala. Programare cu numere naturale si liste in Coq. (Oc, Oab, Oat) Lecture, discussion, giving examples/ Prelegere, conversatie, exemplificare Slides/ Slide-uri : https://members.loria.fr/SStratulat/files/MVA/MVA-Introduction.pdf Interactive web page / Pagina web interactiva : https://members.loria.fr/SStratulat/files/jscoq-builds/lec1.html
C2. (3h) Propositions and predicates (Oc, Oab) / Propozitii si predicate (Oc, Oab) Idem Interactive web page / Pagina web interactiva : https://members.loria.fr/SStratulat/files/jscoq-builds/lec2.html
C3. (3h) Building proofs in Coq (Oc, Oab) / Construirea demonstratiilor in Coq (Oc, Oab) Idem Interactive web page / Pagina web interactiva : https://members.loria.fr/SStratulat/files/jscoq-builds/lec3.html
C4. (3h) Proofs about properties of programs (Oc, Oab) / Demonstratii despre proprietati ale programelor (Oc, Oab) Idem Interactive web page / Pagina web interactiva : https://members.loria.fr/SStratulat/files/jscoq-builds/lec4.html
C5. (4h) Inductive data types (Oc, Oab) / Tipuri de date inductive (Oc, Oab) Idem Interactive web page / Pagina web interactiva : https://members.loria.fr/SStratulat/files/jscoq-builds/lec5.html
C6. (4h) Inductive properties (Oc, Oab) / Proprietati inductive (Oc, Oab) Idem Interactive web page / Pagina web interactiva : https://members.loria.fr/SStratulat/files/jscoq-builds/lec6.html
C7 (4h). Inductive properties – second part – (Oc, Oab) / Proprietati inductive – partea a doua - (Oc, Oab) Idem Interactive web page / Pagina web interactiva : https://members.loria.fr/SStratulat/files/jscoq-builds/lec8.html
C8 (4h). Recursive functions in Coq (Oc, Oab) / Functii recursive in Coq (Oc, Oab) Idem Interactive web page / Pagina web interactiva : https://members.loria.fr/SStratulat/files/jscoq-builds/lec9.html

Course bibliography

A. Appel. Verified Functional Algorithms. 2018 https://softwarefoundations.cis.upenn.edu/vfa-current/index.html Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer Verlag. 2004 https://www.labri.fr/perso/casteran/CoqArt/ A. Chlipala. Certified Programming with Dependent Types. MIT Press. 2013 http://adam.chlipala.net/cpdt/

Seminar content

Content Methods Obs
L1. (2h) How to program with natural numbers and lists in Coq / Exercitii despre programarea cu numere naturale si liste in Coq Problem presentation, discussion, collaborative learning / Problematizare, dialog, invatare prin colaborare Interactive web page / Pagina web interactiva : https://members.loria.fr/SStratulat/files/jscoq-builds/lab1.html
L2. (2h) How to deal with propositions and predicates in Coq / Exercitii despre propozitii si predicate. Idem Interactive web page / Pagina web interactiva : https://members.loria.fr/SStratulat/files/jscoq-builds/lab2.html
L3. (2h) How to build proofs in Coq / Exercitii despre construirea demonstratiilor in Coq Idem Interactive web page / Pagina web interactiva : https://members.loria.fr/SStratulat/files/jscoq-builds/lab3.html
L4. (2h) How to reason about properties of programs / Exercitii despre proprietati ale programelor Idem Interactive web page / Pagina web interactiva : https://members.loria.fr/SStratulat/files/jscoq-builds/lab4.html
L5. (2h) How to deal with inductive data types in Coq / Exercitii despre tipuri de date inductive Idem Interactive web page / Pagina web interactiva : https://members.loria.fr/SStratulat/files/jscoq-builds/lab5.html
L6. (2h) How to deal with inductive properties in Coq / Exercitii despre proprietati inductive Idem Interactive web page / Pagina web interactiva : https://members.loria.fr/SStratulat/files/jscoq-builds/lab6.html
L7. (2h) How to deal with recursive functions in Coq / Exercitii despre functii recursive Idem Interactive web page / Pagina web interactiva : https://members.loria.fr/SStratulat/files/jscoq-builds/lab9.html
Bibliography: CEA-EDF-INRIA summer school. Modelling and Verifying Algorithms in Coq - an introduction. 2011 http://www.di.ens.fr/~zappa/teaching/coq/ecole11/
Bibliography: The content can be correlated with the activities of verification and validation of critical applications / Continutul cursului poate fi corelat cu activitatile de verificare si validare a aplicatiilor critice.

Seminar bibliography

(none)

Corroboration

(none)

AI tools guidance

(none)

Evaluation and delivery

Activity Criteria Methods Percentage
C
  • To describe data structures, algorithms and their properties using a theorem prover, as well as proving these properties (Oc) / Capacitatea de a descrie structuri de date, algoritmi, cat si proprietatile lor utilizand un demonstrator de teoreme, cat si sa demonstreze aceste proprietati (Oc)
  • Written exam / Examen scris in sesiunea de examene
  • 50.0%
S
  • To formalize and verify applications in Coq (Oab) / Capacitatea de a formaliza si a verifica aplicatii in Coq (Oab)
  • Oral exam of a project / Evaluare orala a proiectului software (tema semestriala)
  • 50.0%

Performance standards

Minimal standard (Knowledge and skills required to get the mark of 5) Ability to write a simple application in Understanding of the basic principles of the activities of modeling and verifying algorithms in Coq. The final mark is computed as the average of the marks obtained for the components 10.4 and 10.5. The exam is passed if the average is at least 5 (it is not required that each mark be greater than 5). To each exam periods, the final mark is computed using this rule. For the exams following a failure or for upgrading a mark, the student can choose one of the two kinds of examination (written or oral), or both. Standard minim (cunoștințe și aptitudini necesare pentru nota 5) Capacitate de a scrie o aplicatie simpla in Coq. Intelegerea principiilor de baza ale activitatilor de modelare si verificare a algoritmilor in Coq. Nota finală se calculează ca medie ponderată a notelor acordate pentru componentele specificate la 10.4 și 10.5. Examenul se consideră promovat dacă media este cel puțin 5 (nu e necesar ca fiecare notă să fie mai mare de 5) . La fiecare dintre sesiunile de examen (inclusiv cele de restanță și măriri) nota se calculează după aceeași regulă. In sesiunea de restanțe/măriri se pot da doar una din cele doua probe (scris sau oral), cu excepția cazului în care studentul dorește să susțină ambele probe.

Additional info

(none)