Pragmatic Quotient Types in Coq

DOI10.1007/978-3-642-39634-2_17zbMath1317.68207OpenAlexW25515096MaRDI QIDQ5327346

Cyril Cohen

Publication date: 7 August 2013

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01966714/file/main.pdf

zbMATH Keywords

formalization of mathematicsCoqquotient types

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (12)

Tests and proofs for custom data generators ⋮ Quotients of Bounded Natural Functors ⋮ Trakhtenbrot’s Theorem in Coq ⋮ Formalizing the Face Lattice of Polyhedra ⋮ Regular language representations in the constructive type theory of Coq ⋮ Quotients by Idempotent Functions in Cedille ⋮ Unnamed Item ⋮ Graph theory in Coq: minors, treewidth, and isomorphisms ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Formalizing complex plane geometry

Uses Software

• Coq

This page was built for publication: Pragmatic Quotient Types in Coq