|
Программные системы: теория и приложения, 2014, том 5, выпуск 3, страницы 27–50
(Mi ps122)
|
|
|
|
Эта публикация цитируется в 3 научных статьях (всего в 3 статьях)
Математические основы программирования
O зависимых типах и интуиционизме в программировании математики
С. Д. Мешвелиани Институт программных систем им. А. К. Айламазяна РАН, Ярославская обл., Переславский район, с. Веськово
Аннотация:
Обсуждается практическая возможность доказуемого программирования математики на основе подхода конструктивизма и применения языка с зависимыми типами (dependent types, proof carrying code). Принципы конструктивизма и доказуемого программирования объясняются на примерах. Рассмотрение опирается на опыт реализации на языке Agda небольшой библиотеки вычислительной алгебры, включающей арифметику области остатков $R/(b)$ для евклидова кольца $R$.
Ключевые слова и фразы:
конструктивная математика, алгебра, зависимые типы, Coq, Agda, Haskell.
Образец цитирования:
С. Д. Мешвелиани, “O зависимых типах и интуиционизме в программировании математики”, Программные системы: теория и приложения, 5:3 (2014), 27–50
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/ps122 https://www.mathnet.ru/rus/ps/v5/i3/p27
|
Статистика просмотров: |
Страница аннотации: | 252 | PDF полного текста: | 177 | Список литературы: | 36 |
|