Skip to Main content Skip to Navigation
Conference papers

Pragmatic Quotient Types in Coq

Cyril Cohen 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : In intensional type theory, it is not always possible to form the quotient of a type by an equivalence relation. However, quotients are extremely useful when formalizing mathematics, especially in algebra. We provide a Coq library with a pragmatic approach in two complementary components. First, we provide a framework to work with quotient types in an axiomatic manner. Second, we program construction mechanisms for some specific cases where it is possible to build a quotient type. This library was helpful in implementing the types of rational fractions, multivariate polynomials, field extensions and real algebraic numbers.
Document type :
Conference papers
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Cyril Cohen Connect in order to contact the contributor
Submitted on : Saturday, December 29, 2018 - 2:55:57 PM
Last modification on : Thursday, January 20, 2022 - 5:30:45 PM
Long-term archiving on: : Saturday, March 30, 2019 - 1:18:18 PM


Files produced by the author(s)


  • HAL Id : hal-01966714, version 1



Cyril Cohen. Pragmatic Quotient Types in Coq. International Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.16. ⟨hal-01966714⟩



Les métriques sont temporairement indisponibles