LINUX.ORG.RU

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


1

4

Как люди разрабатывают семантику для языков программирования? Пишут на бумажке, затем прототип и смотрят получилось ли?

Наткнулся, к примеру, на библиотеку для Racket: Redex что есть ещё на эту тему?

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

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

> cast jtootf, quasimoto

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

anonymous ()

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

Видимо, да. Можно считать это около математической деятельностью. И сами формальные семантики часто - переформулировки моделей уже известных в математике (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

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

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

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

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

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

vladimir-vg ★★ ()

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

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

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

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

quasimoto ★★★★ ()
Ответ на: комментарий от vladimir-vg

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

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

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

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

vladimir-vg ★★ ()
Ответ на: комментарий от vladimir-vg

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

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

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

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

jtootf ★★★★★ ()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.