Coq without type casts: a complete proof of Coq Modulo Theory

DOI10.29007/BJPGzbMATH Open1403.68227OpenAlexW2739481936MaRDI QIDQ4645754FDOQ4645754

Authors: Jean-Pierre Jouannaud, Pierre-Yves Strub 

Publication date: 10 January 2019

Published in: EPiC Series in Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.29007/bjpg

Recommendations

• scientific article; zbMATH DE number 6680163
• Coq Modulo Theory
• Computer Science Logic
• Theory of types and decision procedures
• scientific article; zbMATH DE number 1361477

zbMATH Keywords

type theoryCoqproof assistantsoundnessfirst-order theory

Mathematics Subject Classification ID

Cited In (7)

• Computer Science Logic
• Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
• Coq Modulo Theory
• An extensible equality checking algorithm for dependent type theories
• Tactics for Reasoning Modulo AC in Coq
• Equality, quasi-implicit products, and large eliminations
• Equality checking for general type theories in Andromeda 2

Uses Software

• Coq
• CoqMTU
• CoqMT

This page was built for publication: Coq without type casts: a complete proof of Coq Modulo Theory

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