Аннотация доклада.

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