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]

Authors

Ariel Kellison

This author has not been identified. Look up 'Ariel Kellison' in Google

Mark Bickford

This author has not been identified. Look up 'Mark Bickford' in Google

Robert L. Constable

This author has not been identified. Look up 'Robert L. Constable' in Google