JetBrains Research — наука, меняющая мир

Семантика рекурсивных типов с индексацией шагов исполнения

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

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

Докладчик: Дима Розплохас

Материалы

Andrew W. Appel, David Allen McAllester. An indexed model of recursive types for foundational proof-carrying code. Transactions on Programming Languages and Systems, 2001. https://dl.acm.org/doi/10.1145/504709.504712

Семинар пройдет онлайн 19 октября в 17:30, ссылка Google meet: https://meet.google.com/myu-dhmz-gvu