Язы́к программи́рования — формальный язык, предназначенный для записи компьютерных программ. Язык программирования определяет набор лексических, синтаксических и семантических правил, определяющих внешний вид программы и действия, которые выполнит исполнитель под её управлением.
Функциона́льное программи́рование — парадигма программирования, в которой процесс вычисления трактуется как вычисление значений функций в математическом понимании последних.
OCaml — объектно-ориентированный язык функционального программирования общего назначения. Был разработан с учётом безопасности исполнения и надёжности программ. Поддерживает функциональную, императивную и объектно-ориентированную парадигмы программирования. Самый распространённый в практической работе диалект языка ML.
Standard ML (SML) — компилируемый язык программирования общего назначения высшего порядка, основанный на системе типов Хиндли — Милнера.
Предметно-ориентированный язык — компьютерный язык, специализированный для конкретной области применения. Построение такого языка и/или его структура данных отражают специфику решаемых с его помощью задач. Является ключевым понятием языково-ориентированного программирования.
Фри́дрих Лю́двиг Го́тлоб Фре́ге — немецкий логик, математик и философ. Представитель школы аналитической философии.
Рудольф Ка́рнап — немецко-американский философ и логик, ведущий представитель логического позитивизма в философии науки.
L4 — микроядро второго поколения, разработанное Йохеном Лидтке в 1993 году.
Coq — интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования (Gallina) с зависимыми типами. Позволяет записывать математические теоремы и их доказательства, удобно модифицировать их, проверяет их на правильность. Пользователь интерактивно создаёт доказательство сверху вниз, начиная с цели. Coq может автоматически находить доказательства в некоторых ограниченных теориях с помощью так называемых тактик. Coq применяется для верификации программ.
В 1991 году были различные научные и технологические события, некоторые из которых представлены ниже.
Языково-ориентированное программирование (ЯОП), также Расходящаяся разработка, также метаязыковая абстракция, также Разработка, опирающаяся на предметно-специфичный язык — парадигма программирования, заключающаяся в разбиении процесса разработки программного обеспечения на стадии разработки предметно-ориентированных языков (DSL) и описания собственно решения задачи с их использованием. Стадии могут вестись последовательно или параллельно, однократно или рекурсивно; DSL могут быть реализованы зависимо или независимо от базового языка и иметь одну или множество реализаций.
MLton — кроссплатформенный полнопрограммно-оптимизирующий компилятор языка программирования Standard ML (SML). Как и большинство остальных реализаций Standard ML, написан на самом Standard ML и распространяется с открытыми исходными кодами под лицензией в стиле BSD.
Логика разделения, сепарационная логика — формальная система, субструктурная логика, применимая к верификации программ, содержащих изменяемые структуры данных и указатели, расширение логики Хоара. Разработана Джоном Рейнольдсом, Питером О’Хирном, Самином Иштиаком и Хонсёком Яном на основе работ Рода Бёрстола. Язык утверждений логики разделения является специальным случаем логики пучковых импликаций.
Типобезопасность — свойство языка программирования, характеризующее безопасность и надёжность в применении его системы типов.
Язык модулей ML — система модулей, используемая преимущественно в языках программирования семейства ML, имеющая аппликативную семантику, иначе говоря, представляющая собой небольшой функциональный язык, оперирующий модулями.
Формальная верификация криптографических протоколов — проверка криптографических протоколов на обеспечение требуемых свойств безопасности. Одной из составляющих такой проверки является определение стойкости протокола к атакам в предположении о надёжности криптографических примитивов, на которых он основывается. Для решения этой задачи разработан ряд подходов, основанных на различных формальных методах верификации. Общей чертой формальных методов является использование системного подхода к проблеме, позволяющего выполнять более обоснованную, точную и эффективную проверку свойств безопасности протокола.
Оскар Иоахим Беккер — немецкий философ, логик, математик, историк математики. Наряду с Мартином Хайдеггером он — один из наиболее выдающихся учеников Эдмунда Гуссерля. В числе его учеников Макс Бенсе, Пауль Лоренцен, Ганс Слуга, Юрген Хабермас, Карл-Отто Апель, Карл-Хайнц Ильтинг, Герман Шмитц, Элизабет Штрёкер и Отто Пёггелер. Профессор в Бонне. Представитель феноменологического метода, внес вклад в философию экзистенциализма постановкой вопроса о «параэкзистенции» в сфере внечеловеческого. Отстаивал конструктивистскую позицию, во многом близкую интуционизму, по истории математики.
Isabelle — интерактивный инструмент для автоматического доказательства, использующий логику высшего порядка. Реализован в том же стиле, что и один из первых подобных инструментов — LCF и, точно так же как и LCF, был первоначально полностью написан на языке Standard ML. Система содержит компактное логическое ядро, которое можно принимать в качестве истинного без дополнительных доказательств. Как универсальный инструмент, реализует металогику, которая используется для реализации нескольких вариантов логики объектов Isabelle, таких как логика первого порядка (FOL), логика высшего порядка (HOL) или теория множеств Цермело-Френкеля (ZFC). Чаще всего используется вариант объектной логики является Isabelle/HOL, так же достаточно серьёзные разработки в области теории множеств проводились с использованием Isabelle/ZF.
Logic for Computable Functions, (LCF) — инструмент для интерактивного автоматического доказательства теорем, разработанный Робином Милнером и его сотрудниками в Стэнфорде и Эдинбурге в начале 1970-х годов на базе одноимённой дедуктивной системы, предложенной Даной Скоттом. В ходе работы над системой LCF был разработан универсальный язык программирования ML. Его применение в системе позволило пользователям писать тактики доказательства теорем, поддерживающие алгебраические типы данных, параметрический полиморфизм, абстрактные типы данных и исключения.
Инструмент интерактивного доказательства теорем — программное обеспечение, помогающее исследователю в разработке формальных доказательств. Доказательства вырабатываются в процессе взаимодействия человека с машиной. Как правило, такое программное обеспечения включает в себя какую-то разновидность интерактивного редактора доказательств или другой интерфейс, с помощью которого человек может вести поиск доказательств, сведения о которых хранятся в компьютере, а также процедуры автоматической проверки доказательств, осуществляемые компьютером.