Наряду с исследованиями в различных направлениях системного программирования в Отделе велись работы в области теоретического программирования, основы которых были заложены А.П. Ершовым. Его позиция заключалась в том, что серьезные эксперименты по созданию систем должны подкрепляться разработкой теоретических моделей и стимулировать эту разработку.
В.К. Сабельфельд, И.В. Поттосин, В.Е. Котов,
А.П. Ершов, В.Н. Касьянов
Опыт в трансляторных проектах вызвал естественный интерес к теории схем программ - как последовательных, так и параллельных. Работы по схемам программ концентрировались вокруг проблем эквивалентности и преобразований схем Янова. А.П. Ершовым и его учениками (В.Э. Иткиным, В.К. Сабельфельдом, Э.Л. Горель) был получен ряд интересных результатов: был найден общий критерий локальности правил преобразований схем Янова, доказана логическая независимость правил преобразования, построена полная система преобразований с отношением тождества, доказана распознаваемость логико-термальной эквивалентности и пр. Для стандартных схем программ В.А. Непомнящим предложены новые классы с разрешимыми проблемами пустоты и тотальности. Для стандартных схем с интерпретациями - операторных алгоритмов, введенных и изученных А.П. Ершовым, В.А. Непомнящий установил критерии алгоритмической полноты систем операций, что было существенным продвижением в решении проблемы, поставленной А.П. Ершовым и А.А. Ляпуновым. В.А. Непомнящий и Н.В. Шилов разработали схемный метод разрешения пропозициональных динамических логик.
В области теории параллельного программирования классические результаты принадлежат В.Е. Котову и А.С. Нариньяни: они предложили одну из первых моделей параллельных программ - недетерминированные асинхронные автоматы, и для этой модели получили ряд важных результатов, связанных с условиями отсутствия конфликтов параллелизма, с преобразованием последовательных программ в параллельные и преобразованиями, увеличивающими внутренний параллелизм. Работы в этой области продолжали В.В. Вальковский, И.Б. Вирбицкайте и ее ученики.
Лаборатория теоретического программирования ИСИ сейчас развивает эти идеи и получает новые результаты по спецификации и верификации параллельных и распределенных программ.
А.В. Быстровым, Г.И. Алексеевым, С.П. Мыльниковым и Т.Г. Чуриной под руководством В.А. Непомнящего создана система анализа и симуляции сетевых моделей "NetCalc". Это экспериментальный интегрированный программный комплекс для проектирования, анализа и симуляции сетевых моделей распределенных систем. Модели строятся на основе сетей Петри и их разнообразных обобщений. Комплекс включает: настраиваемый графический редактор иерархических сетевых структур; анализатор структурных и поведенческих свойств моделей; блок имитационного моделирования и отладки. Упомянутыми сотрудниками, а также С.А. Куртовым, Е.В. Окунишниковой и П.А. Чубаревым была разработана и реализована система EPV верификации Estelle-спецификаций коммуникационных протоколов, которая базируется на системе NetCalc.
А.А. Сулимовым и И.С. Ануреевым, под руководством В.А. Непомнящего разработана проблемно-ориентированная система верификации программ СПЕКТР. На вход экспериментальной системы СПЕКТР подается аннотированная программа (с входным и выходным условиями и инвариантами циклов). Система проверяет соответствие программы ее спецификациям.
Для коллектива, активно работающего в области трансляции, естественным было обратить внимание на теорию оптимизации программ и на применение этой теории для создания оптимизирующих трансляторов. А.П. Ершовым (совместно с С.С. Лавровым) были заложены основы современной теории экономии памяти. Был предложен ряд моделей программ, ориентированных на обоснование других оптимизирующих преобразований. Модель линейных схем, предложенная И.В. Поттосиным, позволяла обосновывать преобразования, связанные с удалением и перестановкой операторов, что было использовано в системе БЕТА. Модель линейных программ, также разработанная И.В. Поттосиным, позволила построить оптимальный алгоритм преобразования линейных участков. В.Н. Касьяновым была предложена и более общая модель крупноблочных схем, объединяющая возможность линейных схем и преобразований, связанных с памятью.
Впоследствии эти работы вылились в исследования по специализации программ - А.П. Ершовым был предложен принцип смешанных вычислений, который дал толчок потоку исследований в разных коллективах в мире. В ИСИ продолжение работ в этой области привело к появлению экспериментального специализатора алголоподобного языка программирования MixLan, созданного М.А. Бульонковым и Д.В. Кочетовым.
Система предназначена для специализации экспериментального языка программирования MixLan, являющегося подмножеством языка Алгол-68 и допускающего эквивалентный перевод в себя языков Паскаль, Модула-2, Си.
Анализатор семантических свойств (АСС), разработанный В.К. Сабельфельдом и П.Г. Емельяновым, предназначен для статического анализа семантических свойств методом абстрактной интерпретации программ. Информация, выявленная во время анализа, предназначена для обнаружения семантических ошибок времени исполнения, документирования, оптимизации и конкретизации программ.
В работах В.Н. Касьянова сформулирован ряд общих концепций конструирования качественных программ посредством конкретизирующих преобразований, определяющих дальнейшее развитие трансформационного программирования как одного из основных методов доказательного программирования.
И.В. Поттосин и В.Н. Касьянов обосновали важную технологическую роль оптимизирующих преобразований при решении задач автоматизации программирования в целом.
Теоретические исследования в этой области поддерживаются созданием экспериментальных систем конструирования качественных программ на основе аннотирования программ и конкретизирующих преобразований. Созданы конкретизатор программ ТРАП, система конкретизации СКАТ, информационно-поисковая система ТРАНСФОРМ и др.