[λ] Инструменты для описания семантики.

coq? у Пирса есть пример описания операционной семантики, и изучения её свойств

cast jtootf, quasimoto

> cast jtootf, quasimoto

Не понял. Тебе-таки нужен ответ от алгебраика или от корчевателя?

Пишут на бумажке, затем прототип и смотрят получилось ли?

Видимо, да. Можно считать это около математической деятельностью. И сами формальные семантики часто - переформулировки моделей уже известных в математике (haskell - system F, agda и coq - теория типов Мартина-Лёфа, cyclone - линейные типы и).

Рассуждения о семантиках и верификации реализаций могут проводится тоже формально и с помощью proof ассистентов.

Некоторые ссылки в порядке релевантности (ссылки по ссылкам тоже подойдут):

http://pauillac.inria.fr/~xleroy/courses/Marktoberdorf-2009/

http://pauillac.inria.fr/~xleroy/courses/Eugene-2010/

http://liyang.hu/work.xhtml

http://www.cse.chalmers.se/~nad/publications/danielsson-dtp2010-talk.html

http://www.cis.upenn.edu/~bcpierce/attapl/

http://arxiv.org/abs/0710.2505

Не понял. Тебе-таки нужен ответ от алгебраика или от корчевателя?

cast-таки сработал :)

Прошёл по одной из ссылок, пропал на час. Круто, интересно.

> coq? у Пирса есть пример описания операционной семантики, и изучения её свойств

Да, спасибо, анонимус. Ты про вот это: http://www.cis.upenn.edu/~bcpierce/sf/toc.html ?

Внесу свои пять копеек

http://media.ccc.de/browse/conferences/camp2011/cccamp11-4426-certified_progr...

http://adam.chlipala.net/cpdt/

ЗЫ: В Coq используется Calculus of Inductive Constructions, а не теория типов Мартина-Лёфа.

ммм.. какая интересная тема: столько ссылок... внесу ка я ее в избранное. =)

В Coq используется Calculus of Inductive Constructions, а не теория типов Мартина-Лёфа.

CoC это (импредикативная) её разновидность.

Ещё такую штуку вспомнил - http://www.cs.berkeley.edu/~megacz/coq-in-ghc/.

я ни разу не специалист - для меня формальные методы остановились на рассмотрении операционной семантики в процессе проектирования. ссылки из треда тоже утащу, почитаю на досуге :)

> ни разу не специалист - для меня формальные методы остановились на рассмотрении операционной семантики в процессе проектирования

А в на чём ты специализируешься, чем интересуешься? Вообще было бы неплохо сделать перекличку энтузиастов CS.

А в чём ты специализируешься

в написании программ :) в массе своей - всякая более или менее эмбедщина

чем интересуешься?

алгеброй. от CS как такового я страшно далёк