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/Coq-Equations
A function definition package for Coq
mattam82/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.
mattam82/math-classes
mattam82/coq-opam-archive
Archive for all Coq related OPAM packages organized in various repositories
mattam82/metacoq
Reflection library for Coq
mattam82/alectryon
A collection of tools for writing technical documents that mix Coq code and prose.
mattam82/bonak
🧊 An indexed construction of semi-simplicial and semi-cubical types
mattam82/certicoq
mattam82/color
Coq library on rewriting theory and termination
mattam82/coq-elpi
Coq plugin embedding elpi
mattam82/coq-ext-lib
A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
mattam82/coq-malfunction
mattam82/coqhammer
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
mattam82/cross-crypto
Connecting computational and symbolic crypto models
mattam82/dockercoq
Docker files for particular Coq builds with packages
mattam82/fiat
Mostly Automated Synthesis of Correct-by-Construction Programs
mattam82/HoTT
Homotopy type theory
mattam82/malfunction
Malfunctional Programming
mattam82/metacoq_plugins
mattam82/nixpkgs
Nix Packages collection
mattam82/perennial
Verifying concurrent crash-safe systems
mattam82/platform
Multi platform setup for Coq, Coq libraries and tools
mattam82/platform-docs
A project of short tutorials and how-to guides for Coq features and Coq Platform packages.
mattam82/QuickChick
Randomized Property-Based Testing Plugin for Coq
mattam82/relation-algebra
Relation algebra library for Coq
mattam82/rewriter
Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
mattam82/SquiggleEq
mattam82/vscode-git-grep
Git grep extension for Visual Studio Code
mattam82/VST
Verified Software Toolchain
mattam82/www
Sources files of the coq.inria.fr website (static part)