PROGRAM SYSTEMS: THEORY AND APPLICATIONS

12+

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

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