Заседание No. 37, Подход конструктивной математики и зависимых типов в программировании алгебры

Докладчик: Сергей Давидович Мешвелиани (ИПС им. А.К. Айламазяна РАН)
Дата: 16th October 2015
Время: 13:00
Место: зал ученого совета ИПС
Презентация: Download
Annotation:

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