LINUX.ORG.RU
Форум — Development  

Формальная верификация

 ,


1

1

Привет!

Я заинтересовался языками с зависимыми типами. Попробовал писать на Agda, но она мне не очень понравилась. Переключился на Coq. Начал читать Software Fuondations и решать задания оттуда.

Русскоязычных материалов по Coq практически нет. В ЖЖ есть gds и deni_ok, тут и на хабре есть ymn.

Что почитать по основам Coq? Язык английский, русский.

Какой простенький проект подойдет для новичка?

← Скорости разработки и исполнения, не достижимые на С
Unknown CMake command «QT4_ADD_RESOURCES». →
Ответ на: комментарий от betalor

меня зря, я на Coq не писал и вряд ли смогу что-то подсказать

jtootf ★★★★★
()

Какой простенький проект подойдет для новичка?

Перепиши стандартную прелюдию так, чтобы по крайней мере все рекурсивные схемы были выражены через комонады.

anonymous
()

Coq

русский

Ага, раскатал губу.

anonymous
()

typical anonymous comment

функциональное питушение
//ну а вобще тоже интересно)))

Bad_ptr ★★★★★
()

Заняться нечем что ли? Быдлокодь иди.

З.Ы.: а чем Agda не понравилась?

anonymous
()
Ответ на: комментарий от anonymous

Тем что дрянь хаскелеподобная для школьнгиков.

anonymous
()

Если Software Foundations, то интересуют именно применения к верификации «обычных» программ, а не просто математика, правильно я понял? Тогда к SF можно ещё добавить CPDT. Из проектов — посмотреть на CompCert (написан большей частью на Coq) и на Frama-C (можно использовать Coq как внешней прувер, та же Inria участвовала).

Насчёт агды — в Coq, в принципе, всё так же будет, даже где-то топорнее (сам Thierry Coquand агду использует в своих курсах). С ней можно почитать более общего характера книги, как введения именно в технику доказательств — http://www.csie.ntu.edu.tw/~b94087/ITT.pdf, http://www.cse.chalmers.se/research/group/logic/book/book.pdf, ну и потом http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials, http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Publications. Вот использовать code extraction с ней более проблематично (хотя можно), так что она больше подойдёт для отдельного моделирования без прямой кодогенерации (http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Libraries, http://www.cse.chalmers.se/~nad/repos/, https://github.com/liyang/stm-proof).

quasimoto ★★★★
()

Материалов на русском языке нет. Когда я читал Пирса, то делал некоторые заметки, которые время от времени перевожу в электронный вид. Брать тут. Там треш и угар, но пулл-реквесты принимаются)

Читай Пирса и параллельно CPDT. Решай упражнения из SF.

ymn ★★★★★
()
12 января 2014 г.

Учи французский, читай Coq'Art.

anonymous
()
Ответ на: комментарий от jtootf

Я про http://www.cse.chalmers.se/edu/year/2013/course/DAT140_Types, хотя это не совсем его курс и только один. В публикациях и то и другое можно увидеть (но, опять, они в соавторстве, например с Danielsson — Agda, для ForMath — Coq, так что каких-то явных предпочтений не просматривается).

quasimoto ★★★★
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.
← Скорости разработки и исполнения, не достижимые на С
Development
Unknown CMake command «QT4_ADD_RESOURCES». →