package coq-metacoq-safechecker

Overview
Homepage

You can search for identifiers within the package.

in-package search v0.2.0

Implementation and verification of safe conversion and typechecking algorithms for Coq

Install

Dune Dependency

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

Authors

A

Abhishek Anand <[email protected]>
D

Danil Annenkov <[email protected]>
S

Simon Boulier <[email protected]>
C

Cyril Cohen <[email protected]>
Y

Yannick Forster <[email protected]>
J

Jason Gross <[email protected]>
F

Fabian Kunze <[email protected]>
M

Meven Lennon-Bertrand <[email protected]>
K

Kenji Maillard <[email protected]>
G

Gregory Malecha <[email protected]>
J

Jakob Botsch Nielsen <[email protected]>
M

Matthieu Sozeau <[email protected]>
N

Nicolas Tabareau <[email protected]>
T

Théo Winterhalter <[email protected]>

Maintainers

M

[email protected]

Sources

v1.3.4-9.0.tar.gz

sha512=0243145ea97a99532da856b28b1bdd99f7db083cddfd04855b3b298611b894f6e14aa0628f0a236e9893a5a69f1a82b8af94ed6ea5b5a401fd55f6336230a8d8

Description

MetaCoq is a meta-programming framework for Coq.

The SafeChecker modules provides a correct implementation of weak-head reduction, conversion and typechecking of Coq definitions and global environments.

Published: 03 Apr 2025

Dependencies (1)

coq-metacoq-pcuic = version

Dev Dependencies

None

Used by (4)

coq-elm-extraction
coq-metacoq-erasure >= "1.3.4+9.0"
coq-metacoq-safechecker-plugin >= "1.3.4+9.0"
coq-rust-extraction

Conflicts

None

On This Page

Description
Dependencies (1)
Dev Dependencies
Used by (4)
Conflicts