MetaCoq

MaRDI QIDQ55704swMATHFDO

Official website https://metacoq.github.io

Source code repository https://github.com/MetaCoq/metacoq

Described by source

• The \textsc{MetaCoq} project

Cited in

(18)

• \texttt{slepice}: towards a verified implementation of type theory in type theory
• Mtac
• TCB
• CertiKOS
• Autosubst
• CertiCoq
• HOLCF
• OEuf
• Template-Coq
• HOL Light QE
• Logipedia
• Metamath Zero
• PLM
• coq-library-undecidability
• Translation certification for smart contracts
• Extracting functional programs from Coq, in Coq
• Cubical Agda
• LogiKEy

This page was built for software: MetaCoq