package coq-metacoq-pcuic

  1. Overview
  2. No Docs
A type system equivalent to Coq's and its metatheory

Install

Dune Dependency

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

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

metacoq-1.3.2-8.20.tar.gz
sha512=df2552795eab097c779e1e70d5f7f14a7e1b696d0ce42d1929f7a8b6ffc1a26a93d9e2bdcaf462c9d326c040efa57d1f3daa3fe953afcf6a18075d04d5ee3298

Description

MetaCoq is a meta-programming framework for Coq.

The PCUIC module provides a cleaned-up specification of Coq's typing algorithm along with a certified typechecker for it. This module includes the standard metatheory of PCUIC: Weakening, Substitution, Confluence and Subject Reduction are proven here.

Published: 06 Sep 2024

Dependencies (1)

  1. coq-metacoq-common = version

Dev Dependencies

None

Conflicts

None