Repositories list

• htt

  Public
  Hoare Type Theory

  Coq

  •66 forks•00 stars•00 issues•00 pull requests•Updated Jan 16, 2025Jan 16, 2025

• proofengineering.github.io

  Public
  Studying Software Engineering in the Proof Assistant world.

  HTML

  •00 forks•77 stars•66 issues•00 pull requests•Updated Jul 4, 2020Jul 4, 2020

• regmatch

  Public
  Certified regular expression matcher in Coq

  regexpcoqssreflect+ 1

  regexpcoqssreflectmathcomp

  Coq

  •00 forks•44 stars•00 issues•00 pull requests•Updated Mar 17, 2020Mar 17, 2020

• proofengineering-bib

  Public
  BibTeX bibliographies for proof engineering-related papers

  bibtexbibliographybibtex-db+ 1

  bibtexbibliographybibtex-dbproof-engineering

  TeX

  •

  Other

  •11 fork•3030 stars•00 issues•00 pull requests•Updated Jul 24, 2019Jul 24, 2019

• opam-repository-dev

  Public
  Proof engineering development package repository for OPAM

  00 forks•00 stars•00 issues•00 pull requests•Updated Jul 21, 2019Jul 21, 2019

• atbr-plugin

  Public
  Coq

  •00 forks•00 stars•00 issues•00 pull requests•Updated Jul 21, 2019Jul 21, 2019

• coq

  Public
  Coq with extensions for proof engineering

  OCaml

  •

  GNU Lesser General Public License v2.1

  •721721 forks•11 star•00 issues•00 pull requests•Updated Jun 13, 2019Jun 13, 2019

• coq-dpdgraph

  Public
  Build dependency graphs between COQ objects

  Coq

  •

  GNU Lesser General Public License v2.1

  •3434 forks•00 stars•00 issues•00 pull requests•Updated May 3, 2019May 3, 2019

• serapi-tests

  Public
  Some Coq regression tests for SerAPI

  Coq

  •00 forks•00 stars•00 issues•00 pull requests•Updated Nov 25, 2018Nov 25, 2018

• coq-docker

  Public archive
  Dockerfiles with various versions of Coq

  Roff

  •11 fork•11 star•11 issue•00 pull requests•Updated Sep 30, 2018Sep 30, 2018

• reglang

  Public archive
  OPAM friendly version of files from the paper Regular Language Representations in the Constructive Type Theory of Coq

  Coq

  •00 forks•00 stars•00 issues•00 pull requests•Updated Sep 23, 2018Sep 23, 2018

• coqhammer

  Public archive
  A fork of the CoqHammer proof automation plugin

  OCaml

  •

  Other

  •00 forks•11 star•00 issues•00 pull requests•Updated Sep 23, 2018Sep 23, 2018

• ott

  Public
  Ott is a tool for writing definitions of programming languages and calculi

  OCaml

  •

  Other

  •5353 forks•00 stars•00 issues•00 pull requests•Updated Apr 27, 2018Apr 27, 2018

• UniMath

  Public
  This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

  Coq

  •

  Other

  •187187 forks•00 stars•00 issues•00 pull requests•Updated Jan 17, 2018Jan 17, 2018

• proofengineering-doc

  Public
  Documentation related to proof engineering

  00 forks•33 stars•00 issues•00 pull requests•Updated Dec 20, 2017Dec 20, 2017

• coqproject-legacy

  Public archive
  Shell

  •66 forks•00 stars•00 issues•00 pull requests•Updated Dec 9, 2017Dec 9, 2017

• icoq

  Public
  A regression proof selection tool for the Coq proof assistant

  continuous-integrationcoqproof+ 1

  continuous-integrationcoqproofregression-proof-selection

  Shell

  •11 fork•00 stars•00 issues•00 pull requests•Updated Dec 1, 2017Dec 1, 2017

• opam-repository

  Public
  Proof engineering released package repository for OPAM

  00 forks•00 stars•00 issues•00 pull requests•Updated Nov 17, 2017Nov 17, 2017

• coq-depends

  Public
  Coq plugin for plain dependency extraction

  dependency-analysiscoqcoq-plugin

  dependency-analysiscoqcoq-plugin

  OCaml

  •

  GNU Lesser General Public License v2.1

  •11 fork•00 stars•00 issues•00 pull requests•Updated Sep 20, 2017Sep 20, 2017

• coq-ast

  Public
  Coq plugin for printing term abstract syntax trees and their digests

  coqsyntax-treedigest+ 1

  coqsyntax-treedigestcoq-plugin

  OCaml

  •

  Other

  •00 forks•77 stars•11 issue•00 pull requests•Updated Sep 20, 2017Sep 20, 2017