On dependent types and intuitionism in programming mathematics
Abstract
It is discussed a practical possibility of a provable programming of mathematics basing on intuitionism and the dependent types feature of a programming language.The principles of constructive mathematics and provable programming are illustrated with examples taken from algebra. The discourse follows the experience in designing in Agda a computer algebra library DoCon-A, which deals with generic algebraic structures and also provides the needed machine-checked proofs. This paper is a revised translation of a certain paper published in Russian in 2014.
Cite
@article{arxiv.1709.01810,
title = {On dependent types and intuitionism in programming mathematics},
author = {Sergei D. Meshveliani},
journal= {arXiv preprint arXiv:1709.01810},
year = {2017}
}
Comments
17 pages. A revised translation of a paper published in Russian in "Program systems: theory and applications", Vol. 5, No 3(21), 2014, pages 27 -- 50. http://psta.psiras.ru/read/psta2014_3_27-50.pdf