2017/09/06 by Meshveliani, Sergei D.
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1709.01810
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.