Теория языков программирования

В некотором смысле история теории языка программирования предшествует даже развитию самих языков программирования. В частности, λ-исчисление, разработанное Алонзо Чёрчем и Стивеном Клини в 1930-х годах, фактически является первым языком программирования, даже при том, что оно было предназначено больше для теоретических вопросов вычислимости, нежели является средством для программистов; многие современные функциональные языки программирования являются вариантами λ-исчисления. Дальнейшая история теории тесно переплетена с историей языков программирования, при этом в рамках теоретических исследований создавались новые парадигмы, конструкции и методы, а результаты внедрения их в практические языки программирования обеспечивали обратную связь для развития теории.

Первым языком программирования, который был изобретён для применения в действующей электронно-вычислительной машине, считается Планкалкюль Конрада Цузе, однако не получил известности у современников (изучен лишь в 1970-е годы и реализован в 1990-е годы). Первым же широко известным и успешным языком программирования стал Фортран (1954—1957), разработанный командой исследователей IBM во главе с Джоном Бэкусом. Успех Фортрана привёл к формированию комитета учёных, которые пытались разработать «универсальный» компьютерный язык; результатом их усилия был Алгол-58. Параллельно Джон Маккарти из MIT разработал язык программирования Лисп (основанный на λ-исчислении), который является первым успешным языком академически проработанной теоретической основой. К 1950-м годам относятся разработка иерархии Хомского, оказавшая непосредственное влияние теорию языков программирования.

В 1964 году Питер Лэндин впервые реализовал вариант λ-исчисления, которое могло быть использовано для моделирования языков программирования (SECD-машина и J-оператор, по существу являющийся разновидностью продолжения). В 1966 году Лэндин разработал абстрактный язык программирования ISWIM.

В 1966 году Коррадо Бёмом и Джузеппе Якопини (итал. Giuseppe Jackopini) доказана теорема, согласно которой алгоритм может быть преобразован к виду, использующему только три структуры управления — последовательной, ветвление и цикл, впоследствии этот результат стал теоретическим фундаментом структурного программирования. В созданном Оле-Йоханом Далем и Кристеном Нюгором в 1967 году языке Симула был разработан, как полагают, первый пример языка объектно-ориентированного программирования и введено понятие сопрограммы. Важной вехой в развитии направления стал курс лекций Fundamental Concepts in Programming Languages Кристофера Стрейчи (англ. Christopher Strachey), выпущенный в 1967 году, где, кроме систематизации знаний по теории языков программирования, глубоко исследовано понятие полиморфизма. Значительный вклад в становление понятия о типах в языках программирования связывают с работой 1969 года Роджера Хиндли, результаты которой вылились обобщённый в алгоритм вывода типов.

В 1969 году Тони Хоар разработал логику Хоара — первый пример аксиоматической семантики для языков программирования, обеспечивающей формальную верификацию программного кода. В 1970 году Даной Скоттом разработана денотационная семантика.

В 1972 году создана парадигма логического программирования и язык Пролог, в котором программа состоит непосредственно из набора хорновских дизъюнктов. Другой областью интересов теоретиков языков программирования начала 1970-х годов стало внедрение абстрактных типов данных на уровне конструкций языка, первым таким языком считается Клу (1974, Барбара Лисков).

Важной вехой на пути становления парадигмы функционального программирование стала разработка независимо Жираром (фр. Jean-Yves Girard; 1971) и Рейнольдсом (англ. John C. Reynolds; 1974) системы F — типизированного λ-исчисления второго порядка, обеспечивающего возможность конструирования термов, зависящих от типов. Также заметный вклад в развитие функционального программирования в середине 1970-х годов внесён разработчиками языка программирования Scheme — диалекта Лисп, включившего лексическую область видимости, объединённое пространство имён и элементы из модели акторов, в том числе продолжения. Подъём широкого интереса к функциональному программированию связан с тьюринговской лекцией создателя Фортрана Бэкуса 1977 года, в которой он критически проанализировав состояние популярных на тот момент языков программирования пришёл к функциональной парадигме.

В 1980 году Уильям Ховард (англ. William Alvin Howard), ссылаясь на труды логика Хаскелла Карри 1950-х годов, выявил структурное соответствие между компьютерными программами и математическими доказательствами, ставшее известным как изоморфизм Карри — Ховарда и ставшего теоретической основой класса языков автоматического доказательства.

В первую половину 1980-х годов значительное внимание уделено исследованиям по воплощению параллелизма в языках программирования и разработкам вариантов исчисления процессов: созданы исчисление взаимодействующих систем (Милнер, 1980), язык взаимодействующих последовательных процессов (Хоар, 1985), окончательно сформировалась модель акторов Хьюитта (англ. Carl Hewitt).

Выпуск языка Миранда в 1985 году подогрел академический интерес к ленивым чистым функциональным языкам программирования, в результате был создан комитет для определения открытого стандарта такого языка, в итоге в 1990 году вышел стандарт версии 1.0 языка Haskell.

В 1986 году в рамках работ по созданию языка Eiffel создана парадигма контрактного программирования (Бертран Мейер, 1986).

Теория изучает аспекты языков программирования, насколько это возможно, как совокупности, используя тот или иной конкретный язык как пример, но при этом задействуя средства достаточно высокого уровня общности, для возможности применения результатов к некоторому классу языков. Часто в теоретических разработках создаётся некоторый специализированный, «академический» язык программирования, не пригодный в силу тех или иных причин для практической реализации, но демонстрирующий те или иные теоретические результаты, которые впоследствии применяются к используемым в отрасли языкам. Для теоретических исследований используется инструментарий оснований математики и математической логики, включая теорию множеств, теорию моделей, теорию вычислимости, а также таких абстрактных разделов, как теория категорий, универсальная алгебра, теория графов, и существенно зависит от результатов прикладных направлений, в том числе теории сложности вычислений, теории кодирования.

• Хронология языков программирования
• Поколения языков программирования

• https://web.archive.org/web/20170125145344/http://foswiki.cs.uu.nl/foswiki/Techno/ProgrammingLanguageTheoryTextsOnline
• Abadi, Martín and Cardelli, Luca. A Theory of Objects. Springer-Verlag.
• Michael J. C. Gordon. Programming Language Theory and Its Implementation. Prentice Hall.
• Gunter, Carl and Mitchell, John C. (eds.). Theoretical Aspects of Object Oriented Programming Languages: Types, Semantics, and Language Design. MIT Press.
• Harper, Robert. Practical Foundations for Programming Languages. Draft version.
• Knuth, Donald E. (2003). Selected Papers on Computer Languages. Stanford, California: Center for the Study of Language and Information.
• Mitchell, John C.. Foundations for Programming Languages.
• Mitchell, John C.. Introduction to Programming Language Theory.
• O’Hearn, Peter. W. and Tennent, Robert. D. (1997). Algol-like Languages. Progress in Theoretical Computer Science. Birkhauser, Boston.
• Pierce, Benjamin C. (2002). Types and Programming Languages. MIT Press.
• Pierce, Benjamin C. Advanced Topics in Types and Programming Languages.
• Pierce, Benjamin C. et al. (2010). Software Foundations.

• Computer Languages History (англ.)
• Lambda the Ultimate, a community weblog for professional discussion and repository of documents on programming language theory.
• Great Works in Programming Languages. Collected by Benjamin C. Pierce (University of Pennsylvania).
• Classic Papers in Programming Languages and Logic. Collected by Karl Crary (Carnegie Mellon University).
• Programming Language Research. Directory by Mark Leone.
• Programming Language Theory Texts Online. At Utrecht University.
• λ-Calculus: Then & Now by Dana S. Scott for the ACM Turing Centenary Celebration
• Grand Challenges in Programming Languages. Panel session at POPL 2009.