По направлению к COQ'у

[deniok]

Simon Peyton Jones, Chung-Chieh Shan и Oleg Kiselyov обещают статью "Fun with type functions", а пока выложили слайды. После впечатляющих примеров на Хаскелле с использованием индексированных семейств типов и функций над типами, радует замечание на последнем слайде:

At some point it may be best to say “enough fooling around: just use Coq”. But we aren’t there yet.

Хорошее, годное замечание.

Comments

[deni-ok.livejournal.com]

Похоже пропустил. Спасибо за ссылку!