Мягкое введение в Coq: структуры данных и функции высших порядков

[skiedr]

Думаю все же стоит начинать с введения в object caml, на котором написан coq.

[ymn]

По окамлу есть хорошая литература на русском языке. Однако, я считаю, что знание окамла не обязательно. Гораздо важнее знание некоторых основ математики: теория множеств, логика.

[maxim_ge]

Большое спасибо за статьи, как раз думал немного поизучать Coq.

Вопрос — а есть ли формализация на Coq, скажем, курса школьной геометрии?