Pragmatic Quotient Types in Coq

DOI10.1007/978-3-642-39634-2_17zbMATH Open1317.68207OpenAlexW25515096MaRDI QIDQ5327346FDOQ5327346

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

Coqformalization of mathematicsquotient types

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (14)

• Graph theory in Coq: minors, treewidth, and isomorphisms
• Title not available (Why is that?)
• Tests and proofs for custom data generators
• Title not available (Why is that?)
• Quotients by Idempotent Functions in Cedille
• Regular language representations in the constructive type theory of Coq
• Quotients of Bounded Natural Functors
• Title not available (Why is that?)
• Formalizing complex plane geometry
• Trakhtenbrot’s Theorem in Coq
• Formalizing the Face Lattice of Polyhedra
• Title not available (Why is that?)
• Practical Proof Search for Coq by Type Inhabitation
• Satisfiability modulo finite fields

Uses Software

• Coq

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5327346)