package coq-coq-in-coq

  1. Overview
  2. Homepage
A formalisation of the Calculus of Construction

Install

Dune Dependency

github.com Edit opam file Versions (6)

Authors

  1. B
    Bruno Barras

Maintainers

  1. H
    Hugo.Herbelin@inria.fr

Sources

v8.10.0.tar.gz
md5=d5364ff958bc18ebe91b0e1b10452bc7

Description

Tags

keyword: calculus of constructions category: Mathematics/Logic/Type theory category: Miscellaneous/Extracted Programs/Type checking unification and normalization

Published: 07 Dec 2019

Dependencies (3)

  1. coq >= "8.10" & < "8.11~"
  2. ocaml
  3. camlp5

Dev Dependencies

None

Used by

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