Metaprogramming, verified meta-theory and implementation of Coq in Coq
We're happy to announce the first beta release of the MetaCoq project for Coq 8.11 and 8.12, available both as sources and as opam packages. See the website for introductory material and related articles and presentations.
MetaCoq was formerly called Template-Coq, but now also includes a (work-in-progress) formalisation of Coq in Coq, a verified type checker for Coq, and a verified type and proof erasure procedure, besides the tools for manipulating Coq terms and developing certified plugins (i.e. translations, compilers or tactics) in Coq provided by Template-Coq.
You can install it directly from sources or by typing opam install coq-metacoq
.
The current release includes several subpackages, which can be compiled and installed separately if wanted:
template-coq
and as coq-metacoq-template
)checker
/ coq-metacoq-checker
), usable as MetaCoq Check test
.pcuic
/ coq-metacoq-pcuic
)safechecker
/ coq-metacoq-safechecker
), usable as MetaCoq SafeCheck test
erasure
/ coq-metacoq-erasure
), usable as MetaCoq Erase test
translation
/ coq-metacoq-translations
).A good place to start are the files demo.v
, safechecker_test.v
, erasure_test.v
in the test-suite
directory.
MetaCoq is developed by Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Gregory Malecha, Matthieu Sozeau, Nicolas Tabareau and Théo Winterhalter. You are welcome to contribute by opening issues, PRs or asking questions on Zulip.
The MetaCoq Team
We're happy to announce the first beta release of the MetaCoq project for Coq 8.11 and 8.12, available both as sources and as opam packages. See the website for introductory material and related articles and presentations.
MetaCoq was formerly called Template-Coq, but now also includes a (work-in-progress) formalisation of Coq in Coq, a verified type checker for Coq, and a verified type and proof erasure procedure, besides the tools for manipulating Coq terms and developing certified plugins (i.e. translations, compilers or tactics) in Coq provided by Template-Coq.
You can install it directly from sources or by typing opam install coq-metacoq
.
The current release includes several subpackages, which can be compiled and installed separately if wanted:
template-coq
and as coq-metacoq-template
)checker
/ coq-metacoq-checker
), usable as MetaCoq Check test
.pcuic
/ coq-metacoq-pcuic
)safechecker
/ coq-metacoq-safechecker
), usable as MetaCoq SafeCheck test
erasure
/ coq-metacoq-erasure
), usable as MetaCoq Erase test
translation
/ coq-metacoq-translations
).A good place to start are the files demo.v
, safechecker_test.v
, erasure_test.v
in the test-suite
directory.
MetaCoq is developed by Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Gregory Malecha, Matthieu Sozeau, Nicolas Tabareau and Théo Winterhalter. You are welcome to contribute by opening issues, PRs or asking questions on Zulip.
The MetaCoq Team
We're happy to announce the second alpha release of the MetaCoq project for Coq 8.10 and 8.11, available both as sources and as opam packages. See the website for introductory material and related articles and presentations.
MetaCoq was formerly called Template-Coq, but now also includes a (work-in-progress) formalisation of Coq in Coq, a verified type checker for Coq, and a verified type and proof erasure procedure, besides the tools for manipulating Coq terms and developing certified plugins (i.e. translations, compilers or tactics) in Coq provided by Template-Coq.
You can install it directly from sources or by typing opam install coq-metacoq
.
The current release includes several subpackages, which can be compiled and installed separately if wanted:
template-coq
and as coq-metacoq-template
)checker
/ coq-metacoq-checker
), usable as MetaCoq Check test
.pcuic
/ coq-metacoq-pcuic
)safechecker
/ coq-metacoq-safechecker
), usable as MetaCoq SafeCheck test
erasure
/ coq-metacoq-erasure
), usable as MetaCoq Erase test
translation
/ coq-metacoq-translations
).A good place to start are the files demo.v
, safechecker_test.v
, erasure_test.v
in the test-suite
directory.
MetaCoq is developed by Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Gregory Malecha, Matthieu Sozeau, Nicolas Tabareau and Théo Winterhalter. Please contribute by opening issues or asking questions on gitter.
Best, The MetaCoq Team
We're happy to announce the second alpha release of the MetaCoq project for Coq 8.10 and 8.11, available both as sources and as opam packages. See the website for introductory material and related articles and presentations.
MetaCoq was formerly called Template-Coq, but now also includes a (work-in-progress) formalisation of Coq in Coq, a verified type checker for Coq, and a verified type and proof erasure procedure, besides the tools for manipulating Coq terms and developing certified plugins (i.e. translations, compilers or tactics) in Coq provided by Template-Coq.
You can install it directly from sources or by typing opam install coq-metacoq
.
The current release includes several subpackages, which can be compiled and installed separately if wanted:
template-coq
and as coq-metacoq-template
)checker
/ coq-metacoq-checker
), usable as MetaCoq Check test
.pcuic
/ coq-metacoq-pcuic
)safechecker
/ coq-metacoq-safechecker
), usable as MetaCoq SafeCheck test
erasure
/ coq-metacoq-erasure
), usable as MetaCoq Erase test
translation
/ coq-metacoq-translations
).A good place to start are the files demo.v
, safechecker_test.v
, erasure_test.v
in the test-suite
directory.
MetaCoq is developed by Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Gregory Malecha, Matthieu Sozeau, Nicolas Tabareau and Théo Winterhalter. Please contribute by opening issues or asking questions on gitter.
Best, The MetaCoq Team
Snapshot of MetaCoq - accompanying material of the article:
Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. 2020. Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq. Proc. ACM Program. Lang. 4, POPL, Article 8 (January 2020), 28 pages. https://doi.org/10.1145/3371076
See the README.md file for instructions on how to install and browse the sources.
We're happy to announce the first alpha release of the MetaCoq project for Coq 8.8 and 8.9, available both as sources and as opam packages. See the website for introductory material and related articles and presentations.
MetaCoq was formerly called Template-Coq, but now also includes a (work-in-progress) formalisation of Coq in Coq, a verified type checker for Coq, and a verified type and proof erasure procedure, besides the tools for manipulating Coq terms and developing certified plugins (i.e. translations, compilers or tactics) in Coq provided by Template-Coq.
You can install it directly from sources or by typing opam install coq-metacoq
.
The current release includes several subpackages, which can be compiled and installed separately if wanted:
template-coq
and as coq-metacoq-template
)checker
/ coq-metacoq-checker
), usable as MetaCoq Check test
.pcuic
/ coq-metacoq-pcuic
)safechecker
/ coq-metacoq-safechecker
), usable as MetaCoq SafeCheck test
erasure
/ coq-metacoq-erasure
), usable as MetaCoq Erase test
translation
/ coq-metacoq-translations
).A good place to start are the files demo.v
, safechecker_test.v
, erasure_test.v
in the test-suite
directory.
MetaCoq is developed by Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Gregory Malecha, Matthieu Sozeau, Nicolas Tabareau and Théo Winterhalter. Please contribute by opening issues or asking questions on gitter.
Best, The MetaCoq Team
We're happy to announce the first alpha release of the MetaCoq project for Coq 8.8 and 8.9, available both as sources and as opam packages. See the website for introductory material and related articles and presentations.
MetaCoq was formerly called Template-Coq, but now also includes a (work-in-progress) formalisation of Coq in Coq, a verified type checker for Coq, and a verified type and proof erasure procedure, besides the tools for manipulating Coq terms and developing certified plugins (i.e. translations, compilers or tactics) in Coq provided by Template-Coq.
You can install it directly from sources or by typing opam install coq-metacoq
.
The current release includes several subpackages, which can be compiled and installed separately if wanted:
template-coq
and as coq-metacoq-template
)checker
/ coq-metacoq-checker
), usable as MetaCoq Check test
.pcuic
/ coq-metacoq-pcuic
)safechecker
/ coq-metacoq-safechecker
), usable as MetaCoq SafeCheck test
erasure
/ coq-metacoq-erasure
), usable as MetaCoq Erase test
translation
/ coq-metacoq-translations
).A good place to start are the files demo.v
, safechecker_test.v
, erasure_test.v
in the test-suite
directory.
MetaCoq is developed by Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Gregory Malecha, Matthieu Sozeau, Nicolas Tabareau and Théo Winterhalter. Please contribute by opening issues or asking questions on gitter.
Best, The MetaCoq Team
This release reflects the current status of the Coq 8.8 branch of Template-Coq. It is not feature-complete but stability is expected for:
Work is in progress on:
This release significantly departs from and is incompatible with series 1 by Gregory Malecha (see https://github.com/gmalecha/template-coq/releases) and the previous 8.6 and 8.7 versions.
This release reflects the current status of the Coq 8.8 branch of Template-Coq. It is not feature-complete but stability is expected for:
Work is in progress on:
This release significantly departs from and is incompatible with series 1 by Gregory Malecha (see https://github.com/gmalecha/template-coq/releases) and the previous 8.6 and 8.7 versions.
This release reflects the current status of the Coq 8.8 branch of Template-Coq. It is not feature-complete but stability is expected for:
Work is in progress on:
The formalization of the typing derivations, in particular the missing pieces on (co)-fixpoints and inductives. The correctness proofs of the typechecker. This release significantly departs from and is incompatible with series 1 by Gregory Malecha (see https://github.com/gmalecha/template-coq/releases) and the previous 8.6 and 8.7 versions.