Сертифіковане програмування з The Coq Proof Assistant

---

Власник: проф. Григорій ЖОЛТКЕВИЧ, д.т.н., професор кафедр теоретичної та прикладної інформатики факультету математики і інформатики Харківського національного університету імені В.Н. Каразіна, Харків, Україна інформаційних систем факультету прикладної математики та інформатики Львівського національного університету імені Івана Франка, Львів, Україна E-mail: g.zholtkevych@karazin.ua

Цей репозиторій містить навчальні матеріали щодо формальної верифікації програмного забезпечення з використання The Coq Proof Assistant.

Файли цього репозиторію використовувалися при підготовці та викладанні курсів

1. Сертифіковане програмування з The Coq Proof Assistant
2. Надійність програмних систем

для студентів рівня підготовки магістр за спеціальністю F3 "Комп'ютерні науки"

---

Опис файлової структури

README.md - цей файл
.gitignore - файл стандартних git-виключень для Coq
CoqScripts - директорія з прикладами Coq-скриптів

SPSC.v - скрипт проєкту простого стекового обчислювача
TPSC.v - скрипт проєкту типізованого стекового обчислювача
Logic.v - скрипт з моделлю конструктивної логіки висловлювань
Arithmetic.v - скрипт з моделлю арифметики Пеано
Sorting.v - скрипт з теорією алгоритмів сортування

Lectures - тексти лекцій
Tasks - завдання для самоконтролю

Посилання на джерела

1. Adam Chlipala. Certified Programming with Dependent Types
2. Christine Paulin-Mohring. Introduction to the Coq proof-assistant for practical software verification
3. Yves Bertot, Pierre Castéran. Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions
4. Software Foundations (серія робіт, які є вступом до математичних основ надійного програмного забезпечення)