Implementing Euclid's straightedge and compass constructions in type theory

Ariel Kellison, Mark Bickford, Robert L. Constable. Implementing Euclid's straightedge and compass constructions in type theory. Annals of Mathematics and Artificial Intelligence, 85(2-4):175-192, 2019. [doi]

Abstract

Abstract is missing.