Pragmatic Quotient Types in Coq - Archive ouverte HAL Access content directly
Conference Papers Year : 2013

Pragmatic Quotient Types in Coq

(1)
1
Cyril Cohen

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.
Fichier principal
Vignette du fichier
main.pdf (459.37 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01966714 , version 1 (29-12-2018)

Identifiers

  • HAL Id : hal-01966714 , version 1

Cite

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

Collections

INRIA INRIA2
50 View
383 Download

Share

Gmail Facebook Twitter LinkedIn More