Исследовательская группа

Лаборатория языковых инструментов

Full reduction at full throttle

April 26

Внутренняя стратегия вычисления термов в Coq основывается на call-by-value семантике Calculus of Inductive Constructions. Но у этой стратегии есть одна проблема: она не оптимизирована по памяти и времени, поэтому она плохо масштабируется на большие проекты. Поэтому в Coq есть более подходящие для больших проектов стратегии вычисления. Одна из них — native_compute.

В этом докладе мы рассмотрим, как работает эта стратегия вычисления, а именно, посмотрим на то, как эта она переводит термы на языке Gallina в код на OCaml. А в конце посмотрим на то, как работают стратегии вычисления в Coq на различных бенчмарках.

Материалы к докладу:

https://hal.inria.fr/hal-00650940/document

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