PROGRAM SYSTEMS: THEORY AND APPLICATIONS

12+

 

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.

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 •

 

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: info@psta.psiras.ru.      Website: http://psta.psiras.ru

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