Interactive Theorem Proving and Program Development: Texts in Theoretical Computer Science. An EATCS Series

Prezentat sub formă de manual de referință, volumul Interactive Theorem Proving and Program Development constituie o introducere pragmatică în utilizarea asistentului de demonstrație Coq pentru dezvoltarea teoriilor matematice și a software-ului certificat formal. Putem afirma că lucrarea reprezintă un pilon fundamental pentru cercetătorii și inginerii interesați de metode formale, oferind o punte între rigoarea logică și implementarea practică. Structura cărții este riguros organizată în 16 capitole, începând cu fundamentele tipurilor și expresiilor, continuând cu logica de zi cu zi și tipurile de date inductive, și culminând cu subiecte de nișă precum obiectele infinite sau demonstrația prin reflecție. Reținem importanța capitolului dedicat extracției programelor imperative, care demonstrează utilitatea asistentului Coq în producerea de software cu zero defecte. Cititorii familiarizați cu Types for Proofs and Programs de Eduardo Gimenez vor aprecia aici abordarea didactică mult mai aplicată, volumul funcționând nu doar ca o expunere teoretică, ci ca un ghid de lucru veritabil, susținut de numeroase exerciții. În contextul operei autorului, această lucrare consolidează direcția de cercetare explorată de Yves Bertot și în From Semantics to Computer Science, însă cu un accent mult mai pronunțat pe instrumentele de verificare interactivă. Stilul este tehnic și precis, reflectând experiența autorilor în cadrul INRIA, și se adresează unui public academic de nivel masteral sau doctoral, pregătit să exploreze complexitatea calculului construcțiilor inductive.