package coq-metacoq-template-pcuic

  1. Overview
  2. Homepage
Translations between Template Coq and PCUIC and proofs of correctness

Install

Dune Dependency

metacoq.github.io Edit opam file Versions (12)

Authors

  1. A
    Abhishek Anand <aa755@cs.cornell.edu>
  2. D
    Danil Annenkov <danil.v.annenkov@gmail.com>
  3. S
    Simon Boulier <simon.boulier@inria.fr>
  4. C
    Cyril Cohen <cyril.cohen@inria.fr>
  5. Y
    Yannick Forster <forster@ps.uni-saarland.de>
  6. J
    Jason Gross <jgross@mit.edu>
  7. F
    Fabian Kunze <fkunze@fakusb.de>
  8. M
    Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>
  9. K
    Kenji Maillard <kenji.maillard@inria.fr>
  10. G
    Gregory Malecha <gmalecha@gmail.com>
  11. J
    Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com>
  12. M
    Matthieu Sozeau <matthieu.sozeau@inria.fr>
  13. N
    Nicolas Tabareau <nicolas.tabareau@inria.fr>
  14. T
    Théo Winterhalter <theo.winterhalter@inria.fr>

Maintainers

  1. M
    matthieu.sozeau@inria.fr

Sources

v1.2-8.16.tar.gz
sha512=1fc976740f2ff5a6c4137cf4722e09cae5765d0d71f55e6a020883218396856558a6534aa7d2bd192b60778427edbbc2f096a0e738e95551808702613edbbb31

Description

Published: 22 Apr 2023

Dependencies (2)

  1. coq-metacoq-pcuic = version
  2. coq-metacoq-template = version

Dev Dependencies

None

Conflicts

None

Rocq

Interactive Theorem Prover

Zulip GitHub Discourse Mastodon RSS
About
Changelog Releases Industrial Users Academic Users History Why Rocq? Roadmap
Ecosystem
Platform Packages Rocq Team Community Consortium Events Rocq Planet Jobs
Resources
Install Rocq Get Started Documentation Books Papers Logo
Policies
Governance Privacy Code of Conduct