Mixing Computations and Proofs
Beeson, Michael
Journal of Formalized Reasoning, Volume 9 (2016), / Harvested from Journal of Formalized Reasoning

We examine the relationship between proof and computation in mathematics, especially in formalized mathematics. We compare the various approaches to proofs with a significant computational component, including (i) verifying  the algorithms, (ii) verifying the results of the unverified algorithms, and (iii) trusting an external computation.  

Published online : 2016-01-01
DOI : https://doi.org/10.6092/issn.1972-5787/4552
     title = {Mixing Computations and Proofs},
     journal = {Journal of Formalized Reasoning},
     volume = {9},
     year = {2016},
     doi = {10.6092/issn.1972-5787/4552},
     language = {EN},
     url = {http://dml.mathdoc.fr/item/4552}
Beeson, Michael. Mixing Computations and Proofs. Journal of Formalized Reasoning, Volume 9 (2016) . doi : 10.6092/issn.1972-5787/4552. http://gdmltest.u-ga.fr/item/4552/