Skip to content

@proofengineering ProofEngineering

Change the repository type filter

All

    Repositories list

    20 repositories

    • htt

      Public
      Hoare Type Theory
      Coq
      •5•0•0•0•Updated Oct 7, 2024Oct 7, 2024

    • proofengineering.github.io

      Public
      Studying Software Engineering in the Proof Assistant world.
      HTML
      •0•7•6•0•Updated Jul 4, 2020Jul 4, 2020

    • regmatch

      Public
      Certified regular expression matcher in Coq
      regexpssreflectmathcompcoq
      Coq
      •0•4•0•0•Updated Mar 17, 2020Mar 17, 2020

    • proofengineering-bib

      Public
      BibTeX bibliographies for proof engineering-related papers
      bibtexbibliographybibtex-dbproof-engineering
      TeX
      •
      Other
      •1•30•0•0•Updated Jul 24, 2019Jul 24, 2019

    • opam-repository-dev

      Public
      Proof engineering development package repository for OPAM
      0•0•0•0•Updated Jul 21, 2019Jul 21, 2019

    • atbr-plugin

      Public
      Coq
      •0•0•0•0•Updated Jul 21, 2019Jul 21, 2019

    • coq

      Public
      Coq with extensions for proof engineering
      OCaml
      •
      GNU Lesser General Public License v2.1
      •659•1•0•0•Updated Jun 13, 2019Jun 13, 2019

    • coq-dpdgraph

      Public
      Build dependency graphs between COQ objects
      Coq
      •
      GNU Lesser General Public License v2.1
      •28•0•0•0•Updated May 3, 2019May 3, 2019

    • serapi-tests

      Public
      Some Coq regression tests for SerAPI
      Coq
      •0•0•0•0•Updated Nov 25, 2018Nov 25, 2018

    • coq-docker

      Public archive
      Dockerfiles with various versions of Coq
      Roff
      •1•1•1•0•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
      •0•0•0•0•Updated Sep 23, 2018Sep 23, 2018

    • coqhammer

      Public archive
      A fork of the CoqHammer proof automation plugin
      OCaml
      •
      Other
      •0•1•0•0•Updated Sep 23, 2018Sep 23, 2018

    • ott

      Public
      Ott is a tool for writing definitions of programming languages and calculi
      OCaml
      •
      Other
      •45•0•0•0•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
      •173•0•0•0•Updated Jan 17, 2018Jan 17, 2018

    • proofengineering-doc

      Public
      Documentation related to proof engineering
      0•4•0•0•Updated Dec 20, 2017Dec 20, 2017

    • coqproject-legacy

      Public archive
      Shell
      •6•0•0•0•Updated Dec 9, 2017Dec 9, 2017

    • icoq

      Public
      A regression proof selection tool for the Coq proof assistant
      continuous-integrationcoqproofregression-proof-selection
      Shell
      •1•0•0•0•Updated Dec 1, 2017Dec 1, 2017

    • opam-repository

      Public
      Proof engineering released package repository for OPAM
      0•0•0•0•Updated Nov 17, 2017Nov 17, 2017

    • coq-depends

      Public
      Coq plugin for plain dependency extraction
      dependency-analysiscoqcoq-plugin
      OCaml
      •
      GNU Lesser General Public License v2.1
      •1•0•0•0•Updated Sep 20, 2017Sep 20, 2017

    • coq-ast

      Public
      Coq plugin for printing term abstract syntax trees and their digests
      coqsyntax-treedigestcoq-plugin
      OCaml
      •
      Other
      •0•7•1•0•Updated Sep 20, 2017Sep 20, 2017