Книги по семантике языка программирования

Я читал « Семантику с приложениями » от Nielson & Nielson , и мне очень нравится эта тема. Я хотел бы иметь еще одну книгу по семантике языка программирования - но я действительно могу получить только одну.

Я взглянул на книгу « Турбак / Гиффорд» , но она слишком многословна; Я думал, что с Винскелем все будет в порядке, но у меня нет доступа к нему (его нет в нашей университетской библиотеке, и у меня мало денег), и я даже не уверен, что он не датирован. Слоннегер кажется нормальным, но практическая часть делает его слишком длинным, и мне не очень нравится его стиль.

Итак, мой вопрос - Winskel хорошая книга? И это от?

Кроме того, есть ли другие краткие книги на эту тему?

Все зависит от того, насколько глубоко вы хотите зайти, и сколько вы уже знаете. Для новичка книга Винксела действительно хороша, но да, она не знакомит вас с современным уровнем семантики, как она была написана около 20 лет назад. Тем не менее, это хорошее первое знакомство с предметом. Также стоит отметить, что Т. Нипков официально оформил значительную часть книги Уинкеля в Изабель / HOL, см. Здесь . Поэтому, если вы хотите научиться использовать интерактивные помощники по проверке вместе с пониманием семантики языков программирования, у вас есть много связного материала, на который можно опираться.

Другие книги, которые являются более продвинутыми:

• Гюнтер, Семантика языков программирования , более продвинутая книга, посвященная денотационной семантике, подход к семантике, который не оправдал ожиданий. Фокусируется на чисто функциональных языках и игнорирует параллелизм. Это книга, из которой я изучал семантику как студент, и, оглядываясь назад, я бы хотел использовать книгу Винксела. Гюнтер не легок для начинающих.

• Домены и лямбда-исчисления Амадио и Кюриена. Еще одна книга, написанная больше в области теоретико-предметной традиции, хотя в ней обсуждаются исчисления процессов.

• Книги Джона Митчелла, которые уже упоминались выше. Они также в основном касаются последовательных вычислений.

Такие книги, как TAPL Пирса, очень хороши, но сосредоточены на одном аспекте языков программирования, а именно на типах, как бы они ни были важны. Я не рекомендовал бы это как первое введение в общую область языков программирования, но это обязательно для чтения любому, кто хочет узнать о типах.

По правде говоря, я думаю, что в настоящее время нет современной вводной книги по семантике языка, которая отражала бы существенный прогресс, достигнутый за последнее десятилетие, с его решительным переходом от денотационных методов и последовательных вычислений к параллелизму (исчисления процессов и игровая семантика) , аксиоматика семантики и использование интерактивных доказательств помощников при проверке.

Обновление 22. Апрель 2014: Тобиас Нипков и Джервин Кляйн опубликовали новую книгу

• Конкретная семантика

который можно увидеть как «Winskel in Isabelle / HOL». Это введение в семантику языков программирования (прежде всего операционного и аксиоматического), но в отличие от предыдущих подходов, основанных на ручке и бумаге, эта книга выражает всю свою математику в Изабель / HOL. Другими словами, это книга о доказательстве теорем.

Книга совершенно новая, поэтому я не использовал ее для преподавания, но она выглядит действительно подходящей как введение, которое представлено на более низком уровне, чем Software Foundations от Pierce et al.

Вот случайный образец материалов, доступных бесплатно онлайн:

• Винскель, Формальная семантика языков программирования , Google Books превью . Я ничего не знаю об этой книге. Он находится в списке, потому что вопрос конкретно касается его контента, который в основном онлайн.
• Морган, Программирование из спецификации , список файлов ps . Предметом является уточнение, то есть процесс, начиная с высокоуровневых неисполняемых описаний и систематически превращая их во что-то исполняемое. Конечно, каждый шаг уточнения должен сохранять семантику, поэтому в нем также обсуждается определенный тип семантики (в основном на основе предикатных средств преобразования).
• Харпер, Практические основы языков программирования , pdf проекта . Смотрите комментарий Дэйва Кларка ниже.
• Реми, Использование, Понимание и Раскрытие Языка OCaml , pdf . Это книга , из которой я узнал , функциональное программирование (OCaml, точнее) , и мне понравилось это много . Он представляет семантику основных языковых особенностей очень хорошим способом и в процессе представляет лямбда-исчисление и теорию типов на основе «необходимости знать».
• Пейтон Джонс, Реализация языков функционального программирования , DJVU . Первые главы описывают лямбда-исчисление (и его «операционную семантику») и то, как функции языка более высокого уровня дезагрегируются в лямбда-исчисление. В этом смысле статья дает операционную семантику для функциональных языков.
• Пирс (ред.), Расширенные темы по типам и языкам программирования , предварительный просмотр Google Книг .
• Слоннегер, Синтаксис и семантика языков программирования , список файлов PDF . Я смотрел на это коротко давным-давно и мне не очень понравилось. Это в списке, потому что это упоминается в вопросе.
• Брукс, Семантика для параллельной логики разделения , pdf . Это большая статья (80 страниц), а не книга. Я включил это, потому что это довольно недавнее развитие, которое я нахожу интересным.

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

В уже упоминавшейся книге Уинскеля есть оба аспекта. И это хорошая книга для начинающих. Не менее хорошая, возможно, даже лучшая книга - это та, с которой я начал: « Гороскопное описание языков программирования» . Это была моя первая книга по семантике, которую я прочитал вскоре после окончания бакалавриата. Я должен сказать, что это дало мне прочную основу в семантике, и мне никогда не приходилось задумываться о том, чем денотационная семантика отличается от операционной семантики или аксиоматической семантики и т. Д. Эта книга останется моим безоговорочным фаворитом в отношении денотационной семантики.

Другие книги, которые фокусируются на аспектах моделирования, а не на фундаментальных аспектах, являются следующими:

• Tennent в Семантика языков программирования , который является более или менее UpToDate книга по семантике императивных языков программирования. Это легко читать. Тем не менее, он имеет тенденцию быть абстрактным в последующих частях книги, и вам, возможно, придется изо всех сил пытаться понять, почему что-то делается определенным образом.

• Теории языков программирования Рейнольдса . Любой, кто специализируется на семантике, должен обязательно прочитать эту книгу. Это в конце концов Рейнольдс. (Однажды Дэвид Шмидт заметил мне: «Даже если Рейнольдс читает вам утреннюю газету, вы должны внимательно слушать, потому что вы можете узнать что-то важное»!). В ней хорошо освещены как аспекты моделирования, так и основополагающие аспекты.

Лучшими книгами по основополагающим аспектам являются книги Гюнтера (которые я считаю учебником для выпускников) и книги Митчелла (которые являются хорошим справочным пособием на вашей книжной полке, потому что они достаточно всеобъемлющие).

Мне очень понравилось читать Уинкеля, когда я учился на семантическом курсе. Я не могу сказать, датировано ли это, так как я не занимаюсь исследованиями в этой области. Плюсом Winskel является то, что вы можете найти его переведенным на другие языки, кроме английского.

Для дальнейшего чтения, более высокого уровня, я бы предложил книги Джона Митчелла « Основы языков программирования и понятия в языках программирования» . Если вы читаете только первые главы, я думаю, они также отвечают вашим требованиям краткости.

Вы не найдете бесплатных черновиков этих книг, поэтому, если у вас ограниченный бюджет, посмотрите на «мощь» в ответе Раду.

Ну, я не эксперт по этому вопросу, но я могу дать несколько общих советов.

Во-первых, есть люди, которые уже прочитали книгу и предоставили рецензии на нее. Например, для книги Винскеля «Формальная семантика языков программирования» (см. [1] и [2] ) я нашел обзоры на Amazon.

Часть одного обзора гласит:

Эта книга с самого начала путает синтаксис и семантику, как отделение литералов от их значений. Никаких специальных обозначений не использовалось для их дифференциации. Это критически важный вопрос, который автор должен рассмотреть в такой теме. Кроме того, некоторые другие обозначения, которые он использовал, довольно запутанные, например, указание предпосылок и выводов.

Похоже, автор предположил, что у вас есть ВСЕ необходимые предпосылки, поскольку он очень кратко объяснил исходные материалы в первых нескольких главах (то есть теорию множеств, операционную семантику, индукции, индуктивные определения). Стиль, использованный автором во введении, состоит в том, чтобы поместить два или три абзаца текста и поставить некоторые формулы, а затем дать упражнения. Что для меня довольно разочаровывает ...

18/20 человек считают этот отзыв полезным. Вы можете искать Amazon (или другие источники), чтобы увидеть больше отзывов.

Во-вторых, Amazon предлагает вместе с этой книгой типы и языки программирования и теорию базовых категорий для компьютерных ученых . По другой теме Дэйв Кларк предлагает эти книги как отличные по теме «Системы типов и семантика языка программирования». Опять же, я не эксперт, но это может быть полезно для вас.

Я хотел бы добавить две книги, не найденные в ответах, данных до сих пор:

• Аарон Стамп , Фонды языков программирования
• Дэвид Шмидт , денотационная семантика: методология развития языка

Книга Стамп лаконична, но очень ясна.

Для начинающих, изучающих операционную семантику, я бы предложил языки программирования и операционную семантику от Maribel Fernández . Все объясняется очень простым способом, который легко понять. http://www.springer.com/computer/swe/book/978-1-4471-6367-1