Formalizing constructive projective geometry in Agda

DOI10.1016/j.entcs.2018.10.005zbMath1433.68575OpenAlexW2899395665WikidataQ113317510 ScholiaQ113317510MaRDI QIDQ2333313

Guillermo Calderón

Publication date: 12 November 2019

Full work available at URL: https://doi.org/10.1016/j.entcs.2018.10.005

zbMATH Keywords

projective geometrytype theoryAgdaproof assistantsformalizations of mathematics

Mathematics Subject Classification ID

General theory of linear incidence geometry and projective geometries (51A05) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Duality notions in real projective plane

Uses Software

• ALF
• Agda

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A case study in formalizing projective geometry in Coq: Desargues theorem
• The use of projective geometry in computer graphics
• The axioms of constructive geometry
• `Outside' as a primitive notion in constructive projective geometry
• Formalizing Projective Plane Geometry in Coq
• Dependently Typed Programming in Agda
• On the bright side of type classes
• Constructive projective extension of an incidence plane

This page was built for publication: Formalizing constructive projective geometry in Agda