Skip to content

Popular repositories Loading

  1. lambdapi lambdapi Public

    Proof assistant based on the λΠ-calculus modulo rewriting

    OCaml 283 35

  2. Dedukti Dedukti Public

    Implementation of the λΠ-calculus modulo rewriting

    OCaml 200 22

  3. Logipedia Logipedia Public

    An encyclopedia of proofs

    OCaml 57 11

  4. Agda2Dedukti Agda2Dedukti Public

    Haskell 17 4

  5. zenon_modulo zenon_modulo Public

    First-order automated theorem prover based on the tableau method

    OCaml 12 6

  6. SizeChangeTool SizeChangeTool Public

    A termination checker for higher-order rewriting with dependent types

    OCaml 9

Repositories

Showing 10 of 55 repositories
  • lambdapi Public

    Proof assistant based on the λΠ-calculus modulo rewriting

    OCaml 283 35 102 11 Updated Dec 19, 2024
  • coq-hol-light Public

    HOL-Light library in Coq

    Coq 3 1 0 0 Updated Dec 17, 2024
  • hol2dk Public

    HOL-Light to Dedukti/Lambdapi translator

    OCaml 6 3 1 0 Updated Dec 17, 2024
  • lambdapi-stdlib Public

    Repository of Lambdapi developments

    Makefile 5 6 0 2 Updated Dec 10, 2024
  • hol-light Public Forked from jrh13/hol-light

    The HOL Light theorem prover

    OCaml 0 80 0 0 Updated Dec 6, 2024
  • coq-hol-light-real Public

    Translation in Coq of the HOL-Light definition of real numbers

    Coq 0 1 0 0 Updated Dec 6, 2024
  • CoqInE Public

    A Coq plugin to translate Coq proofs into Dedukti terms.

    OCaml 7 LGPL-2.1 4 8 3 Updated Dec 5, 2024
  • zenon_modulo Public

    First-order automated theorem prover based on the tableau method

    OCaml 12 6 3 0 Updated Nov 27, 2024
  • Dedukti Public

    Implementation of the λΠ-calculus modulo rewriting

    OCaml 200 22 39 4 Updated Nov 17, 2024
  • Logipedia Public

    An encyclopedia of proofs

    OCaml 57 11 8 3 Updated Nov 11, 2024