Coq Modulo Theory

DOI10.1007/978-3-642-15205-4_40MaRDI QIDQ3586063zbMATH OpenOpenAlexFDO

Authors Pierre-Yves Strub

Publication date 3 September 2010

Published in Computer Science Logic (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/inria-00497404/file/csl-2010.pdf

Mathematics Subject Classification ID

Recommendations

• Coq without type casts: a complete proof of Coq Modulo Theory
• Mtac: a monad for typed tactic programming in Coq
• Types for Proofs and Programs
• scientific article; zbMATH DE number 6680163
• Mtac: a monad for typed tactic programming in Coq

Cited in

(10)

• First-order automated reasoning with theories: when deduction modulo theory meets practice
• From Sets to Bits in Coq
• Modularity in coalgebra
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
• Tactics for Reasoning Modulo AC in Coq
• Modeling Permutations in Coq for Coccinelle
• Coq without type casts: a complete proof of Coq Modulo Theory
• Confluence: the unifying, expressive power of locality
• Types for Proofs and Programs
• Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules

Describes a project that uses

Uses Software

• Coq
• CoqMT

This page was built for publication: Coq Modulo Theory

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