package coq-metacoq-erasure

  1. Overview
  2. No Docs
Implementation and verification of an erasure procedure for Coq

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 Erasure module provides a complete specification of Coq's so-called "extraction" procedure, starting from the PCUIC calculus and targeting untyped call-by-value lambda-calculus.

The erasure function translates types and proofs in well-typed terms into a dummy tBox constructor, following closely P. Letouzey's PhD thesis.

Published: 06 Sep 2024

Dependencies (2)

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

Dev Dependencies

None

Conflicts

None