Online Scientific Journal published by the Ailamazyan Program Systems Institute of the Russian Academy of Sciences

2014 Issue 1
2014 Issue 2
2014 Issue 3
2014 Issue 4
2014 Issue 5

Papers are accepted in the form of a PDF file

To view the PDF files, you will need Adobe Acrobat Reader


• Содержание выпуска •
• 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 .


Article # 18_2014

24 p.


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.

Ссылка на статью обязательна

• Содержание выпуска •
• Healthcare Information Systems •
• Mathematical Foundations of Programming •


Adress: Ailamazyan Program Systems Institute of the Russian Academy of Sciences, PSTA Online Journal, 4 a Peter the First Street,
Veskovo village, Pereslavl area, Yaroslavl region, 152021 Russia
Phone: +7-4852-695-228.       E-mail:      Website:

© Electronic Scientific Journal "Program Systems: Theory and Applications" 2010-2017
© Ailamazyan Program System Institute of RAS 2010-2018