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

Дата: 16 октября 2015

Время: 13:00

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

Презентация: Скачать

Аннотация:

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