Pragmatic Quotient Types in Coq
From MaRDI portal
Publication:5327346
DOI10.1007/978-3-642-39634-2_17zbMath1317.68207OpenAlexW25515096MaRDI QIDQ5327346
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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
This page was built for publication: Pragmatic Quotient Types in Coq
