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

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

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

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

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

Вычислимость [ править ]

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

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

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

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

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

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

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

• Майкл О. Рабин и Дана С. Скотт
• IBM Journal of Research and Development , vol. 3. С. 114–125, 1959.
• Онлайн-версия

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

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

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

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

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

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

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

О вычислимых числах с приложением к Entscheidungsproblem [ править ]

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

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

Рекурсивные функции [ править ]

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

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

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

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

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

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

Arora & Барака вычислительной сложности и Голдрейха вычислительной сложности (как Кембридж) [ править ]

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

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

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

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

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

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

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

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

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

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

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

• Кук, Стивен А. (1971). "Сложность процедур доказательства теорем" (PDF) . Труды 3-го ежегодного симпозиума ACM по теории вычислений : 151–158. CiteSeerX  10.1.1.406.395 . DOI : 10,1145 / 800157.805047 . S2CID  7573663 .

Описание: в этой статье вводится понятие NP-полноты и доказывается, что проблема логической выполнимости (SAT) является NP-полной . Отметим, что аналогичные идеи были независимо развиты несколько позже Леонидом Левиным в «Левин, Универсальные проблемы поиска. Проблемы передачи информации, 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 .

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

Как создавать случайные функции [ править ]

• Goldreich, O .; Goldwasser, S .; Микали, С. (1986). «Как построить случайные функции» (PDF) . Журнал ACM . 33 (4): 792–807. DOI : 10.1145 / 6490.6503 . S2CID  17064126 .

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

IP = PSPACE [ редактировать ]

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

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

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

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

Описание: эта статья показала, что 21 задача являются NP-Complete, и показала важность этой концепции.

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

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

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

Письмо Гёделя фон Нейману [ править ]

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

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

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

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

Описание: В этой статье вычислительная сложность получила свое название и начало.

Дорожки, деревья и цветы [ править ]

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

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

Теория и приложения секретных функций [ править ]

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

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

Вычислительная сложность [ править ]

• СН Пападимитриу
• Аддисон-Уэсли , 1994, ISBN 0-201-53082-1 

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

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

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

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

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

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

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

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

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

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

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

Алгоритмы [ править ]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

• Киркпатрик, С .; Gelatt, CD; Векки, депутат (1983). «Оптимизация путем имитации отжига». Наука . 220 (4598): 671–680. Bibcode : 1983Sci ... 220..671K . CiteSeerX  10.1.1.123.7607 . DOI : 10.1126 / science.220.4598.671 . PMID  17813860 . S2CID  205939 .

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

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

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

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

Алгоритмы + Структуры данных = Программы [ править ]

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

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

Дизайн и анализ компьютерных алгоритмов [ править ]

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

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

Как решить это с помощью компьютера [ править ]

• Дромей, Р.Г. (1982). Как решить это с помощью компьютера . Prentice-Hall International. ISBN 978-0-13-434001-2.

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

Алгоритмы [ править ]

• Роберт Седжвик
• Аддисон-Уэсли, 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. DOI : 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 . DOI : 10.1147 / rd.214.0350 . Архивировано из оригинального (PDF) 30 мая 2009 года.

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

Теория информации [ править ]

«Математическая теория коммуникации» [ править ]

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

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

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

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

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

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

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

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

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

• Ziv, J .; Лемпель, А. (1977). «Универсальный алгоритм последовательного сжатия данных» . IEEE Transactions по теории информации . 23 (3): 337–343. CiteSeerX  10.1.1.118.8921 . DOI : 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. DOI : 10.1090 / psapm / 019/0235771 . ISBN 9780821813195.

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

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

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

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

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

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

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

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

• Эдвард А. Эшкрофт
• J. Comput. Syst. Sci. 10 (1): 110–135 (1975) doi : 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. DOI : 10,1109 / SFCS.1977.32 . S2CID  117103037 .

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

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

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

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

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

• АВТОМОБИЛЬ Хоар
• 1978 г.

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

Расчет коммуникационных систем [ править ]

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

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

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

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

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

Наука программирования [ править ]

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

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

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

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

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

• АВТОМОБИЛЬ Хоар
• 1985 г.

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

Линейная логика (1987) [ править ]

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

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

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

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

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

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

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

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

Связь и параллелизм [ править ]

• Робин Милнер
• Прентис-Холл Интернэшнл, 1989 г.

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

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

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

Описание: актуальная версия предикативного программирования . Основа для UTP К. Хоара . Самые простые и всесторонние формальные методы.

Ссылки [ править ]