Pinned Repositories
coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
opam
Archive for all Coq related OPAM packages organized in various repositories
Coq-HoTT
A Coq library for Homotopy Type Theory
Constructors
Example Coq plugin
coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Coq-Equations
A function definition package for Coq
Forcing
Forcing layer on top of Coq
groupoid
Internalizing intensional type theory
metacoq
Metaprogramming, verified meta-theory and implementation of Coq in Coq
unicoq
An enhanced unification algorithm for Coq
mattam82's Repositories
mattam82/Constructors
Example Coq plugin
mattam82/groupoid
Internalizing intensional type theory
mattam82/opetopic-coq
Port of Eric Finster's opetopic types to Coq.
mattam82/Coq-unif
Formalization of unification in Coq
mattam82/opam-repository
Main public package repository for OPAM, the source package manager of OCaml.
mattam82/RewriteStrat
Strategical Rewriting plugin
mattam82/typex
XPath formalisation, Alternating automata...
mattam82/aac-tactics
This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainers=@fakusb,@palmskog]
mattam82/bedrock2
A work-in-progress language and compiler for verified low-level programming
mattam82/Categories
mattam82/ceps
Coq Enhancement Proposals
mattam82/company-coq
Company-mode backend for Proof General's coq-mode
mattam82/Coq-Developers-Manual
Additional documentation for the developers of Coq
mattam82/coq-forcing
Tentative implementation of call-by-name forcing in Coq
mattam82/example-plugin
An example Coq plugin
mattam82/fiat-crypto
Cryptographic Primitive Code Generation by Fiat
mattam82/kami
A Platform for High-Level Parametric Hardware Specification and its Modular Verification
mattam82/ltac2
A standalone implementation of Ltac2 as a Coq plugin
mattam82/math-comp
Mathematical Components
mattam82/mattam82.github.io
Build a Jekyll blog in minutes, without touching the command line.
mattam82/Mtac2
mattam82/opam-coq-repo
mattam82/paramcoq
Coq plugin for parametricity
mattam82/plugin_tutorials
A collection of small projects to illustrate how to write plugins for Coq
mattam82/repo-coqs
The repository for Coq versions for developers.
mattam82/repo-unstable
The repository for development packages.
mattam82/Russell
mattam82/smtcoq
Communication between Coq and SAT/SMT solvers
mattam82/translation-mod
A coq plugin implementing the translation associated to a modality
mattam82/UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.