Introduction to applied constructive software verification: Basics (cont'd), Induction

Изучаем математические законы за написанием надёжного софта с целью: делать лучше.

К этому семинару задание — дочитать Basics, прочитать Induction, и сделать все упражнения.

Если что-то не получится или будет непонятно — сформулировать это и спросить на встрече; задание сделано, если оно зелёненькое; проверить всё до курсора — Ctrl-→ в CoqIDE. Так можно прокликивать через каждую тактику.

С собой понадобится ноутбук с CoqIDE или Proof General.

Литература:

• Logical Foundations (softwarefoundations.cis.upenn.edu/c...): наш основной текст
• Вводные слайды Pierce из CIS500 (www.seas.upenn.edu/~cis500/current/...)
• https://github.com/coq/coq/wiki: в том числе ссылки на другие курсы и исследования
• Coq in a hurry (cel.archives-ouvertes.fr/inria-0000...): методичка по базовому Coq
• Certified programming with dependent types (http://adam.chlipala.net/cpdt/): более индустриальный подход к Coq с упором на автоматизацию доказательств (тактики)
• Types and Programming Languages, первый раздел: общий контекст и математика за происходящим
• CS3110 Coq cheatsheet (www.cs.cornell.edu/courses/cs3110/2...): справочник по тактикам

Дальнейшие материалы будут появляться на странице курса (http://iacsv.kocherga.club/) и на форуме (ссылка там же). Пожалуйста, зарегистрируйтесь на форуме — после этого wldhx даст вам доступ к автогрейдеру.

Встреча пройдёт в понедельник 21 января, в 19:30, в антикафе Кочерга.