WikiDer > Список важных публикаций по теоретической информатике

Эта статья поднимает множество проблем. Пожалуйста помоги Улучши это или обсудите эти вопросы на страница обсуждения. (Узнайте, как и когда удалить эти сообщения-шаблоны) Эта статья нужны дополнительные цитаты для проверка. Пожалуйста помоги улучшить эту статью к добавление цитат в надежные источники. Материал, не полученный от источника, может быть оспорен и удален. Найдите источники: «Список важных публикаций по теоретической информатике» – Новости · газеты · книги · ученый · JSTOR (Февраль 2015 г.) (Узнайте, как и когда удалить этот шаблон сообщения) Эта статья возможно содержит оригинальные исследования. Пожалуйста Улучши это к проверка заявленные претензии и добавление встроенные цитаты. Заявления, содержащие только оригинальные исследования, следует удалить. (Февраль 2015 г.) (Узнайте, как и когда удалить этот шаблон сообщения) Эта статья может требовать уборка встретиться с Википедией стандарты качества. Конкретная проблема: список представляет пункт за пунктом без объективной опубликованной поддержки, включая выбор статей из первичной литературы, не подтвержденных источником, устанавливающим их важность (таким образом, составляя РГ: ИЛИ) Пожалуйста помоги улучшить эту статью если вы можете. (Февраль 2015 г.) (Узнайте, как и когда удалить этот шаблон сообщения) (Узнайте, как и когда удалить этот шаблон сообщения)

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

Некоторые причины, по которым конкретная публикация может считаться важной:

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

Вычислимость

Cutland's Вычислимость: введение в теорию рекурсивных функций (Кембридж)

• Катленд, Найджел Дж. (1980). Вычислимость: введение в теорию рекурсивных функций. Издательство Кембриджского университета. ISBN 978-0-521-29465-2.

Обзор этого раннего текста, сделанный Карлом Смитом из Университета Пердью (в Обзоры Общества промышленной и прикладной математики),^[1] сообщает, что это текст с «соответствующей смесью интуиции и строгости… в изложении доказательств», который представляет »фундаментальные результаты классической теории рекурсии [RT]… в стиле… доступном для студентов с минимальным математическим образованием ". Хотя он заявляет, что он «станет отличным вводным текстом для вводного курса в [RT] для студентов-математиков», он предлагает, чтобы «преподаватель был подготовлен к существенному расширению материала…», когда он используется со студентами, изучающими информатику (учитывая недостаток материала о приложениях RT в этой области).^[1]

Разрешимость теорий и автоматов второго порядка на бесконечных деревьях

• Майкл О. Рабин
• Труды Американского математического общества, т. 141, стр. 1–35, 1969

Описание: В документе представлены древовидный автомат, расширение автоматы. Древовидный автомат имел множество применений для доказательства правильность программ.

Конечные автоматы и проблемы их решения

• Майкл О. Рабин и Дана С. Скотт
• Журнал исследований и разработок IBM, т. 3. С. 114–125, 1959.
• Онлайн-версия

Описание: Математическая обработка автоматы, доказательство основных свойств и определение недетерминированный конечный автомат.

Введение в теорию автоматов, языки и вычисления

• Джон Э. Хопкрофт, Джеффри Д. Уллман, и Раджив Мотвани
• Эддисон-Уэсли, 2001, ISBN 0-201-02988-X

Описание: Популярный учебник.

О некоторых формальных свойствах грамматик

• Хомский, Н. (1959). «О некоторых формальных свойствах грамматик». Информация и контроль. 2 (2): 137–167. Дои:10.1016 / S0019-9958 (59) 90362-6.

Описание. В этой статье рассказывается о том, что сейчас известно как Иерархия Хомского, а иерархия сдерживания классов формальные грамматики которые генерируют формальные языки.

О вычислимых числах в приложении к проблеме Entscheidungs.

• Алан Тьюринг
• Труды Лондонского математического общества, Серия 2, т. 42, стр. 230–265, 1937, Дои:10.1112 / плмс / с2-42.1.230.
  Опечатки появились в т. 43, стр. 544–546, 1938, Дои:10.1112 / плмс / с2-43.6.544.
• HTML версия, PDF версия

Описание: Эта статья устанавливает пределы информатики. Он определил Машина Тьюринга, модель для всех вычислений. С другой стороны, она доказала неразрешимость проблема остановки и Entscheidungsproblem и тем самым нашел пределы возможных вычислений.

Рекурсивные функции

• Петер, Рожа (1951). Рекурсивные функции. Академическая пресса. ISBN 9780125526500.

Первый учебник по теория рекурсивных функций. Книга выдержала множество изданий и принесла Петеру Кошута от Венгерский правительство.^[2] Отзывы Рафаэль М. Робинсон и Стивен Клини похвалил книгу за то, что она дает учащимся эффективное начальное введение.^[3]

Представление событий в нервных сетях и конечных автоматах

• С. К. Клини
• Меморандум об исследованиях Rand по проекту ВВС США RM-704, 1951
• Онлайн-версия
• переиздано в: Шеннон, Клод; Маккарти, Джон, ред. (1956). Исследования автоматов. OCLC 564148.

Описание: эта статья представлена конечные автоматы, обычные выражения, и обычные языки, и установили их соединение.

Теория вычислительной сложности

Арора и Барак Вычислительная сложность и Голдрайха Вычислительная сложность (оба Кембриджа)

• Санджив Арора и Боаз Барак, «Вычислительная сложность: современный подход», Cambridge University Press, 2009 г., 579 страниц, твердый переплет
• Одед Голдрайх, "Вычислительная сложность: концептуальная перспектива", Cambridge University Press, 2008 г., 606 страниц, твердый переплет

Помимо уважаемой прессы, представившей эти последние тексты, они получили очень положительные отзывы в Новости ACM SIGACT Дэниел Апон из Университета Арканзаса,^[4] который определяет их как «учебники для курса теории сложности, предназначенные для первых выпускников ... или ... продвинутых студентов бакалавриата ... [с] многочисленными уникальными сильными сторонами и очень немногими недостатками», и заявляет, что оба они:

"отличные тексты, которые полностью охватывают как широту, так и глубину теории вычислительной сложности ... [авторами] ... каждым [кто] является гигантом в теории вычислений [где каждый будет] ... исключительный справочный текст для экспертов в поле ... [и это] ... теоретики, исследователи и преподаватели любой научной школы сочтут любую книгу полезной ".

Рецензент отмечает, что в [Ароре и Бараке] делается определенная попытка включить очень свежий материал, в то время как Голдрайх больше фокусируется на разработке контекстной и исторической основы для каждой представленной концепции », и что он« аплодирует [s ] всем… авторам за их выдающийся вклад ».^[4]

Машинно-независимая теория сложности рекурсивных функций

• Блюм, Мануэль (1967). "Машинно-независимая теория сложности рекурсивных функций" (PDF). Журнал ACM. 14 (2): 322–336. Дои:10.1145/321386.321395.

Описание: Аксиомы Блюма.

Алгебраические методы для интерактивных систем доказательства

• Лунд, К.; Фортноу, Л.; Karloff, H .; Нисан, Н. (1992). «Алгебраические методы для интерактивных систем доказательства». Журнал ACM. 39 (4): 859–868. CiteSeerX 10.1.1.41.9477. Дои:10.1145/146585.146605.

Описание: Эта статья показала, что PH содержится в IP.

Сложность процедур доказательства теорем

• Кук, Стивен А. (1971). «Сложность процедур доказательства теорем» (PDF). Материалы 3-го ежегодного симпозиума ACM по теории вычислений: 151–158. CiteSeerX 10.1.1.406.395. Дои:10.1145/800157.805047.

Описание: В этой статье представлена ​​концепция NP-Полнота и доказал, что Проблема логической выполнимости (SAT) - это NP-Complete. Обратите внимание, что аналогичные идеи были независимо развиты несколько позже Леонид Левин в "Левин, Проблемы универсального поиска. Проблемы передачи информации 9 (3): 265–266, 1973".

Компьютеры и непреодолимость: руководство по теории NP-полноты

• Гарей, Майкл Р.; Джонсон, Дэвид С. (1979). Компьютеры и непреодолимость: руководство по теории NP-полноты. Нью-Йорк: Фриман. ISBN 978-0-7167-1045-5.

Описание: Основное значение этой книги связано с ее обширным списком из более чем 300 NP-Complete проблемы. Этот список стал общей ссылкой и определением. Хотя книга вышла всего через несколько лет после определения концепции, такой обширный список был найден.

Степень сложности вычисления функции и частичное упорядочение рекурсивных множеств

• Рабин, Майкл О. (1960). «Степень сложности вычисления функции и частичное упорядочение рекурсивных множеств» (PDF). Технический отчет № 2. Иерусалим: Еврейский университет.

Описание: Этот технический отчет был первой публикацией, рассказывающей о том, что позже было переименовано. вычислительная сложность^[5]

Насколько хорош симплексный метод?

• Виктор Клее и Джордж Дж. Минти
• Клее, Виктор; Минти, Джордж Дж. (1972). «Насколько хорош симплексный алгоритм?». В кальяне, Овед (ред.). Неравенства III (Труды Третьего симпозиума по неравенству, проходившего в Калифорнийском университете, Лос-Анджелес, Калифорния, 1–9 сентября 1969 г., посвященного памяти Теодора С. Моцкина). Нью-Йорк-Лондон: Academic Press. С. 159–175. МИСТЕР 0332165.CS1 maint: ref = harv (связь)

Описание: Построен куб Клее – Минти в измерении.D, чьи 2^D каждый угол посещают Данцигс симплексный алгоритм за линейная оптимизация.

Как построить случайные функции

• Гольдрайх, О.; Гольдвассер, С.; Микали, С. (1986). «Как построить случайные функции» (PDF). Журнал ACM. 33 (4): 792–807. Дои:10.1145/6490.6503.

Описание: Эта статья показала, что существование односторонние функции приводит к вычислительная случайность.

IP = PSPACE

• Шамир, А. (1992). «IP = PSPACE». Журнал ACM. 39 (4): 869–877. Дои:10.1145/146585.146609.

Описание: IP - это класс сложности, характеристика которого (на основе интерактивные системы доказательства) сильно отличается от обычных вычислительных классов, ограниченных во времени / пространстве. В этой статье Шамир расширил методику предыдущей статьи Лунда и др., Чтобы показать, что PSPACE содержится в IP, и, следовательно, IP = PSPACE, так что каждая проблема одного класса сложности разрешима в другом.

Сводимость комбинаторных задач

• Р. М. Карп
• В редакторах Р. Э. Миллера и Дж. У. Тэтчер, Сложность компьютерных вычислений, Plenum Press, New York, NY, 1972, стр. 85–103.

Описание: Эта статья показала, что 21 различная проблема находятся NP-Complete и показал важность концепции.

Сложность знаний интерактивных систем доказательства

• Гольдвассер, С.; Микали, С.; Рэкофф, К. (1989). «Сложность знаний интерактивных систем доказательства» (PDF). SIAM J. Comput. 18 (1): 186–208. Дои:10.1137/0218012.

Описание: В этой статье представлена ​​концепция нулевое знание.^[6]

Письмо Гёделя фон Нейману

• Курт Гёдель
• Письмо от Гёдель к Джон фон Нейман, 20 марта 1956 г.
• Онлайн-версия

Описание: Гёдель обсуждает идею эффективного универсального средства доказательства теорем.

О вычислительной сложности алгоритмов

• Хартманис, Юрис; Стернс, Ричард (1965). «О вычислительной сложности алгоритмов». Труды Американского математического общества. 117: 285–306. Дои:10.1090 / s0002-9947-1965-0170805-7.

Описание: Эта статья дала вычислительная сложность его имя и семя.

Дорожки, деревья и цветы

• Эдмондс, Дж. (1965). «Дорожки, деревья и цветы». Канадский математический журнал. 17: 449–467. Дои:10.4153 / CJM-1965-045-4.

Описание: существует алгоритм полиномиального времени для поиска максимального совпадения в недвудольном графе и еще один шаг к идее вычислительная сложность. Для получения дополнительной информации см. [2].

Теория и приложения секретных функций

• Яо, А.С. (1982). «Теория и применение секретных функций». 23-й ежегодный симпозиум по основам компьютерных наук (SFCS 1982). С. 80–91. Дои:10.1109 / SFCS.1982.45.

Описание: Эта статья создает теоретическую основу для функции люка и описал некоторые из их приложений, например, в криптография. Обратите внимание, что концепция секретных функций была представлена ​​в «Новых направлениях криптографии» шестью годами ранее (см. Раздел V «Взаимосвязи проблем и лазейки»).

Вычислительная сложность

• C.H. Пападимитриу
• Эддисон-Уэсли, 1994, ISBN 0-201-53082-1

Описание: Введение в теория сложности вычислений, книга объясняет авторскую характеристику P-SPACE и другие результаты.

Интерактивные доказательства и твердость приближающих клик

• Файги, У.; Гольдвассер, С.; Ловас, Л.; Сафра, С.; Сегеди, М. (1996). «Интерактивные доказательства и твердость приближающихся клик». Журнал ACM. 43 (2): 268–292. Дои:10.1145/226643.226652.

Вероятностная проверка доказательств: новая характеристика NP

• Арора, С.; Сафра, С. (1998). «Вероятностная проверка доказательств: новая характеристика NP». Журнал ACM. 45: 70–122. Дои:10.1145/273865.273901.

Проверка доказательства и трудность задач аппроксимации

• Арора, С.; Лунд, К.; Мотвани, Р.; Судан, М.; Сегеди, М. (1998). «Проверка доказательств и трудность задач аппроксимации». Журнал ACM. 45 (3): 501–555. CiteSeerX 10.1.1.145.4652. Дои:10.1145/278298.278306.

Описание: в этих трех статьях был установлен тот удивительный факт, что некоторые проблемы в NP остаются сложными даже тогда, когда требуется только приближенное решение. Видеть Теорема PCP.

Внутренняя вычислительная сложность функций

• Кобэм, Алан (1964). «Внутренняя вычислительная сложность функций» (PDF). Proc. Международного конгресса по логике, методологии и философии науки 1964 г.: 24–30.

Описание: Первое определение класса сложности P. Одна из основополагающих статей теории сложности.

Алгоритмы

«Машинная программа для доказательства теорем»

• Дэвис, М.; Logemann, G .; Лавленд, Д. (1962). «Машинная программа для доказательства теорем» (PDF). Коммуникации ACM. 5 (7): 394–397. Дои:10.1145/368273.368557.

Описание: Алгоритм DPLL. Базовый алгоритм для SAT и других NP-Complete проблемы.

«Машинно-ориентированная логика, основанная на принципе разрешения»

• Робинсон, Дж. А. (1965). «Машинно-ориентированная логика, основанная на принципе разрешения». Журнал ACM. 12: 23–41. Дои:10.1145/321250.321253.

Описание: Первое описание разрешающая способность и объединение используется в автоматическое доказательство теорем; используется в Пролог и логическое программирование.

«Задача коммивояжера и минимальные остовные деревья»

• Хельд, М.; Карп, Р.М. (1970). «Задача коммивояжера и минимальные остовные деревья». Исследование операций. 18 (6): 1138–1162. Дои:10.1287 / opre.18.6.1138.

Описание: Использование алгоритма для минимальное остовное дерево как алгоритм аппроксимации для NP-Complete задача коммивояжера. Алгоритмы приближения стал обычным методом решения проблем NP-Complete.

«Полиномиальный алгоритм в линейном программировании»

• Л. Г. Хачиян
• Советская математика - Доклады, т. 20. С. 191–194, 1979.

Описание: Долгое время не существовало доказуемо полиномиального алгоритма времени для линейное программирование проблема. Хачиян был первым, кто предоставил алгоритм, который был полиномиальным (и не только был достаточно быстрым в большинстве случаев, как предыдущие алгоритмы). Потом, Нарендра Кармаркар представил более быстрый алгоритм на: Нарендра Кармаркар, «Новый алгоритм полиномиального времени для линейного программирования», Комбинаторика, т. 4, вып. 4, стр. 373–395, 1984.

«Вероятностный алгоритм проверки простоты»

• Рабин, М. (1980). «Вероятностный алгоритм проверки простоты». Журнал теории чисел. 12 (1): 128–138. Дои:10.1016 / 0022-314X (80) 90084-0.

Описание: В документе представлены Тест на простоту Миллера-Рабина и изложил программу рандомизированные алгоритмы.

«Оптимизация моделированием отжига»

• Киркпатрик, С.; Gelatt, C.D .; Векки, М. П. (1983). «Оптимизация моделированием отжига». Наука. 220 (4598): 671–680. Bibcode:1983Научный ... 220..671K. CiteSeerX 10.1.1.123.7607. Дои:10.1126 / science.220.4598.671. PMID 17813860.

Описание: В этой статье описывается имитация отжига что сейчас является очень распространенной эвристикой для NP-Complete проблемы.

Искусство программирования

• Дональд Кнут

Описание: Это монография есть четыре тома, посвященные популярным алгоритмам. Алгоритмы написаны на английском и СМЕШИВАНИЕ язык ассемблера (или MMIX язык ассемблера в более поздних выпусках). Это делает алгоритмы понятными и точными. Однако использование язык программирования низкого уровня разочаровывает некоторых программистов, более знакомых с современными структурное программирование языки.

Алгоритмы + Структуры данных = Программы

• Никлаус Вирт
• Прентис Холл, 1976, ISBN 0-13-022418-9

Описание: ранняя и влиятельная книга по алгоритмам и структурам данных, реализованная на языке Паскаль.

Разработка и анализ компьютерных алгоритмов

• Альфред В. Ахо, Джон Э. Хопкрофт, и Джеффри Д. Уллман
• Эддисон-Уэсли, 1974 г., ISBN 0-201-00029-6

Описание: Один из стандартных текстов по алгоритмам примерно за 1975–1985 гг.

Как решить это на компьютере

• Дромей, Р. Г. (1982). Как решить это на компьютере. Prentice-Hall Международный. ISBN 978-0-13-434001-2.

Описание: объясняет Почемуs алгоритмов и структур данных. Объясняет Творческий процесс, то Линия рассуждений, то Факторы дизайна за инновационными решениями.

Алгоритмы

• Роберт Седжвик
• Эддисон-Уэсли, 1983, ISBN 0-201-06672-6

Описание: очень популярный текст по алгоритмам в конце 1980-х годов. Он был более доступным и читабельным (но более элементарным), чем Ахо, Хопкрофт и Ульман. Есть более свежие выпуски.

Введение в алгоритмы

• Томас Х. Кормен, Чарльз Э. Лейзерсон, Рональд Л. Ривест, и Клиффорд Штайн
• 3-е издание, MIT Press, 2009 г., ISBN 978-0-262-03384-8.

Описание: Этот учебник стал настолько популярным, что фактически стал стандартом обучения базовым алгоритмам. Первое издание (с первыми тремя авторами) вышло в 1990 году, второе - в 2001 году, а третье - в 2009 году.

Алгоритмическая теория информации

«О таблицах случайных чисел»

• Колмогоров, Андрей Н. (1963). «О таблицах случайных чисел». Sankhyā Ser. А. 25: 369–375. МИСТЕР 0178484.
• Колмогоров, Андрей Н. (1963). «О таблицах случайных чисел». Теоретическая информатика. 207 (2): 387–395. Дои:10.1016 / S0304-3975 (98) 00075-9. МИСТЕР 1643414.

Описание: Предложен вычислительный и комбинаторный подход к вероятности.

«Формальная теория индуктивного вывода»

• Рэй Соломонов
• Информация и контроль, т. 7. С. 1–22 и 224–254, 1964 г.
• Интернет-копия: часть I, Часть II

Описание: Это было начало алгоритмическая теория информации и Колмогоровская сложность. Обратите внимание, что хотя Колмогоровская сложность назван в честь Андрей Колмогоров, он сказал, что семена этой идеи связаны с Рэй Соломонов. Андрей Колмогоров внес большой вклад в эту область, но в более поздних статьях.

«Алгоритмическая теория информации»

• Чайтин, Григорий (1977). «Алгоритмическая теория информации» (PDF). Журнал исследований и разработок IBM. 21 (4): 350–359. CiteSeerX 10.1.1.48.3094. Дои:10.1147 / rd.214.0350. Архивировано из оригинал (PDF) на 30.05.2009.

Описание: Введение в алгоритмическая теория информации одним из важных людей в этом районе.

Теория информации

«Математическая теория коммуникации»

• Шеннон, К. (1948). «Математическая теория коммуникации». Технический журнал Bell System. 27 (3): 379–423, 623–656. Дои:10.1002 / j.1538-7305.1948.tb01338.x. HDL:10338.dmlcz / 101429.

Описание: Эта статья создала область теория информации.

«Коды обнаружения и исправления ошибок»

• Хэмминг, Ричард (1950). «Коды обнаружения и исправления ошибок». Технический журнал Bell System. 29 (2): 147–160. Дои:10.1002 / j.1538-7305.1950.tb00463.x. HDL:10945/46756.

Описание: В этой статье Хэмминг представил идею код исправления ошибок. Он создал Код Хэмминга и Расстояние Хэмминга и разработали методы доказательства оптимальности кода.

«Метод построения кодов минимальной избыточности»

• Хаффман, Д. (1952). «Метод построения кодов с минимальной избыточностью» (PDF). Труды IRE. 40 (9): 1098–1101. Дои:10.1109 / JRPROC.1952.273898.

Описание: Кодирование Хаффмана.

«Универсальный алгоритм последовательного сжатия данных»

• Зив, Дж.; Лемпель, А. (1977). «Универсальный алгоритм последовательного сжатия данных». IEEE Transactions по теории информации. 23 (3): 337–343. CiteSeerX 10.1.1.118.8921. Дои:10.1109 / TIT.1977.1055714. HDL:10338.dmlcz / 142947. Архивировано из оригинал на 2003-12-04.

Описание: LZ77 алгоритм сжатия.

Элементы теории информации

• Т. Обложка; Дж. Томас (1991). Элементы теории информации. стр.38–42. ISBN 978-0-471-06259-2.

Описание: популярное введение в теорию информации.

Формальная проверка

Присвоение смысла программам

• Флойд, Роберт (1967). Присвоение смысла программам (PDF). Математические аспекты информатики. Материалы симпозиумов по прикладной математике. 19. С. 19–32. Дои:10.1090 / psapm / 019/0235771. ISBN 9780821813195.

Описание: знаменательная статья Роберта Флойда «Присвоение значений программам» вводит метод индуктивных утверждений и описывает, как программа, аннотированная утверждениями первого порядка, может быть продемонстрирована как удовлетворяющая спецификации до и после условия - в документе также вводятся концепции инварианта цикла. и условия проверки.

Аксиоматическая основа компьютерного программирования

• Хоар, К.А.Р. (Октябрь 1969 г.). «Аксиоматическая основа компьютерного программирования» (PDF). Коммуникации ACM. 12 (10): 576–580. Дои:10.1145/363235.363259. Архивировано из оригинал (PDF) на 2016-03-04.

Описание: статья Тони Хоара «Аксиоматическая основа компьютерного программирования» описывает набор правил вывода (то есть формального доказательства) для фрагментов языка программирования, подобного Алголу, описанных в терминах (которые сейчас называются) троек Хора.

Защищенные команды, неопределенность и формальная производная программ

• Дейкстра, Э. В. (1975). «Защищенные команды, неопределенность и формальное происхождение программ». Коммуникации ACM. 18 (8): 453–457. Дои:10.1145/360933.360975.

Описание: В статье Эдсгера Дейкстры «Защищенные команды, недетерминированность и формальная деривация программ» (расширенная его учебником для аспирантов 1976 года «Дисциплина программирования») предлагается, чтобы вместо формальной проверки программы после того, как она была написана (т. Е. Постфактум), программы и их формальные доказательства должны разрабатываться рука об руку (с использованием преобразователей предикатов для постепенного уточнения самых слабых предварительных условий), методом, известным как программное (или формальное) уточнение (или вывод), или иногда «корректность по построению».

Доказательство утверждений о параллельных программах

• Эдвард А. Эшкрофт
• J. Comput. Syst. Sci. 10 (1): 110–135 (1975). Дои:10.1016 / s0022-0000 (75) 80018-3

Описание: статья, в которой представлены доказательства инвариантности параллельных программ.

Техника аксиоматического доказательства для параллельных программ I

• Сьюзан С. Овики, Дэвид Грис
• Акта Информ. 6: 319–340 (1976).

Описание: В этой статье, наряду с работой тех же авторов «Проверка свойств параллельных программ: аксиоматический подход. Commun. ACM 19 (5): 279–285 (1976)», был представлен аксиоматический подход к верификации параллельных программ.

Дисциплина программирования

• Эдсгер В. Дейкстра
• 1976

Описание: Классический учебник Эдсгера Дейкстры для аспирантов «Дисциплина программирования» расширяет его более раннюю статью «Защищенные команды, недетерминированность и формальное создание программ» и твердо устанавливает принцип формального получения программ (и их доказательств) на основе их спецификации.

Денотационная семантика

• Джо Стой
• 1977

Описание: Денотационная семантика Джо Стоя - это первое (для аспирантов) целое изложение математического (или функционального) подхода к формальной семантике языков программирования (в отличие от операционного и алгебраического подходов).

Временная логика программ

• Пнуэли, А. (1977). «Временная логика программ». 18-й ежегодный симпозиум по основам компьютерных наук (SFCS 1977). IEEE. С. 46–57. Дои:10.1109 / SFCS.1977.32.

Описание: Использование темпоральная логика был предложен как метод формальной проверки.

Определение свойств корректности параллельных программ с помощью фиксированных точек (1980)

• Э. Аллен Эмерсон, Эдмунд М. Кларк
• В Proc. 7-й Международный коллоквиум по языкам автоматов и программированию, страницы 169–181, 1980 г.

Описание: проверка модели была представлена ​​как процедура для проверки корректности параллельных программ.

Сообщая последовательные процессы (1978)

• МАШИНА. Hoare
• 1978

Описание: Тони Хоара (оригинал) связь последовательных процессов (CSP) статья представляет идею параллельных процессов (то есть программ), которые не разделяют переменные, а вместо этого взаимодействуют исключительно путем обмена синхронными сообщениями.

Расчет взаимодействующих систем

• Робин Милнер
• 1980

Описание: В статье Робина Милнера A Calculus of Communicating Systems (CCS) описывается алгебра процессов, позволяющая формально рассуждать о системах параллельных процессов, что было невозможно в более ранних моделях параллелизма (семафоры, критические секции, исходный CSP).

Разработка программного обеспечения: строгий подход

• Клифф Джонс
• 1980

Описание: Учебник Клиффа Джонса «Разработка программного обеспечения: строгий подход» - это первое полномасштабное изложение Венского метода разработки (VDM), разработанного (в основном) в исследовательской лаборатории IBM в Вене за предыдущее десятилетие и сочетающего в себе идею программы. доработка согласно Dijkstra с уточнением (или реификацией) данных, посредством которого алгебраически определенные абстрактные типы данных формально преобразуются во все более «конкретные» представления.

Наука программирования

• Дэвид Грис
• 1981

Описание: Учебник Дэвида Гриса «Наука программирования» описывает самый слабый метод предусловия Дейкстры для формального вывода программ, за исключением гораздо более доступного, чем более ранний метод Дейкстры. Дисциплина программирования.

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

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

Связь последовательных процессов (1985)

• МАШИНА. Hoare
• 1985

Описание: Учебник Тони Хоара по взаимодействующим последовательным процессам (CSP) (в настоящее время является третьим наиболее цитируемым справочником по информатике за все время) представляет обновленную модель CSP, в которой взаимодействующие процессы даже не имеют программных переменных и которая, как CCS, позволяет системам процессов рассуждать формально.

Линейная логика (1987)

• Жирар, Ж.-Й (1987). «Линейная логика» (PDF). Теоретическая информатика. 50 (1): 1–102. Дои:10.1016/0304-3975(87)90045-4. Архивировано из оригинал (PDF) 29 ноября 2006 г.

Описание: Жирара линейная логика был прорывом в разработке систем типизации для последовательных и параллельных вычислений, особенно для систем типизации с учетом ресурсов.

Расчет мобильных процессов (1989)

• Р. Милнер, Дж. Парроу, Д. Уокер
• 1989
• Онлайн-версия: Часть 1 и Часть 2

Описание: Эта статья знакомит с Пи-исчисление, обобщение CCS, обеспечивающее мобильность процессов. Исчисление чрезвычайно простое и стало доминирующей парадигмой в теоретическом изучении языков программирования, систем набора текста и логики программ.

Обозначение Z: Справочное руководство

• Спайви, Дж. М. (1992). Обозначение Z: Справочное руководство (2-е изд.). Prentice Hall International. ISBN 978-0-13-978529-0. Архивировано из оригинал на 2016-06-20. Получено 2009-08-24.

Описание: Классический учебник Майка Спайви "Обозначение Z: справочное руководство" обобщает формальный язык спецификаций. Обозначение Z которые, хотя и были созданы Жаном-Раймоном Абриалем, развивались (в основном) в Оксфордском университете за предыдущее десятилетие.

Коммуникация и параллелизм

• Робин Милнер
• Prentice-Hall International, 1989 г.

Описание: Учебник Робина Милнера «Коммуникация и параллелизм» представляет собой более доступное, хотя и все еще технически продвинутое, изложение его более ранних работ по CCS.

Практическая теория программирования

• Эрик Хенер
• Springer, 1993, текущее издание онлайн Вот

Описание: актуальная версия Предикативное программирование. Основа для МАШИНА. HoareUTP. Самые простые и всесторонние формальные методы.

Рекомендации