|
|
 |
• Содержание выпуска •
• Healthcare Information Systems •
• Mathematical Foundations of Programming •
Mathematical Foundations of Programming
Responsible for the Section: doctor of physico-mathematical Sciences
Nikolay Nepeivoda
On the left: assigned number of the paper, submission date, the number
of A5 pages contained in the paper, and the reference to the full-text
PDF
/r1/pdf.jpg) .
|
Article # 18_2014
24
p.
/r2/pdf.jpg)
PDF |
submitted on 04th
Aug 2014 displayed on
website on 29th
Sept
2014
Meshveliani S.D.
On dependent types and intuitionism in programming mathematics
It is discussed a practical possibility of a provable
programming of mathematics basing of the approach of intuitionism, a
language with dependent types, proof carrying code. This approach is
illustrated with examples. The discourse bases on the experience of
implementing in the Agda language of a certain small
algebraic library including the arithmetic of a residue
domain R/(b) for an arbitrary Euclidean ring R. (in
Russian)
Key words: intuitionistic mathematics, algebra, dependent
types, Coq, Agda, Haskell.
|
|
Ссылка на статью
обязательна |
http://psta.psiras.ru/read/psta2014_3_27-50.pdf |
• Содержание выпуска •
• Healthcare Information Systems •
• Mathematical Foundations of Programming •
|
/r5/_derived/content-01(019).en.html_cmp_strtedge110_vbtn.gif){kind=small}
/_derived/content-02(020).en.html_cmp_strtedge110_vbtn.gif){kind=small}
.en.html_cmp_strtedge110_vbtn.gif){kind=small}
/_derived/content-04(022).en.html_cmp_strtedge110_vbtn.gif){kind=small}
/_derived/content-05(023).en.html_cmp_strtedge110_vbtn.gif){kind=small}
