package coq-metacoq-checker

  1. Overview
  2. No Docs
Specification of Coq's type theory and reference checker implementation

Install

Dune Dependency

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

Authors

  1. A
    Abhishek Anand <aa755@cs.cornell.edu>
  2. S
    Simon Boulier <simon.boulier@inria.fr>
  3. C
    Cyril Cohen <cyril.cohen@inria.fr>
  4. Y
    Yannick Forster <forster@ps.uni-saarland.de>
  5. F
    Fabian Kunze <fkunze@fakusb.de>
  6. G
    Gregory Malecha <gmalecha@gmail.com>
  7. M
    Matthieu Sozeau <matthieu.sozeau@inria.fr>
  8. N
    Nicolas Tabareau <nicolas.tabareau@inria.fr>
  9. T
    Théo Winterhalter <theo.winterhalter@inria.fr>

Maintainers

  1. M
    matthieu.sozeau@inria.fr

Sources

v1.0-beta1-8.12.tar.gz
sha256=19fc4475ae81677018e21a1e20503716a47713ec8b2081e7506f5c9390284c7a

Description

MetaCoq is a meta-programming framework for Coq.

The Checker module provides a complete specification of Coq's typing and conversion relation along with a reference type-checker that is extracted to a pluging.

This provides a command: MetaCoq Check [global_reference] that can be used to typecheck a Coq definition using the verified type-checker.

Published: 22 Sep 2020

Dependencies (4)

  1. coq-metacoq-template = version
  2. coq-equations = "1.2.3+8.12"
  3. coq >= "8.12" & < "8.13~"
  4. ocaml >= "4.07.1"

Dev Dependencies

None

Used by (6)

  1. coq-library-undecidability < "1.0.1+8.16"
  2. coq-metacoq = "1.0~beta1+8.12"
  3. coq-metacoq-erasure = "1.0~beta1+8.12"
  4. coq-metacoq-pcuic = "1.0~beta1+8.12"
  5. coq-metacoq-safechecker = "1.0~beta1+8.12"
  6. coq-metacoq-translations = "1.0~beta1+8.12"

Conflicts

None