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

DOI10.29007/BJPGMaRDI QIDQ4645754zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

type theoryCoqproof assistantsoundnessfirst-order theory

Mathematics Subject Classification ID

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

Cited in

(7)

• Computer Science Logic
• Coq Modulo Theory
• Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
• 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

Describes a project that uses

Uses Software

• CoqMT
• CoqMTU
• Coq

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)