Докладчик: Сергей Давидович Мешвелиани (ИПС им. А.К. Айламазяна РАН)

Дата: 16th October 2015

Время: 13:00

Место: зал ученого совета ИПС

Презентация: Download

Annotation:

Обсуждается практическая возможность доказуемого программирования математики на основе подхода конструктивизма и применения языка с зависимыми типами (dependent types, proof carrying code). Принципы конструктивизма и доказуемого программирования объясняются на примерах. Рассмотрение опирается на опыт реализации на языке Agda небольшой библиотеки вычислительной алгебры, включающей арифметику области остатков R/(b) для евклидова кольца R.