Repositories list

• rocq-hollight

  Public
  Translation of HOL-Light libraries in Rocq

  Rocq Prover

  •

  Other

  •2•0•0•0•Updated Jan 23, 2026Jan 23, 2026

• lambdapi

  Public
  Proof assistant based on the λΠ-calculus modulo rewriting

  dependent-typesproof-assistantrewriting+ 3proof-checkerlogical-frameworkproof-translator

  OCaml

  •

  Other

  •40•368•97•17•Updated Jan 22, 2026Jan 22, 2026

• lambdapi-stdlib

  Public
  Repository of Lambdapi developments

  lambdapi

  Lambdapi

  •

  Other

  •9•7•1•7•Updated Jan 22, 2026Jan 22, 2026

• eo2lp

  Public
  Tool for translating Eunoia to LambdaPi

  OCaml

  •1•0•0•0•Updated Jan 21, 2026Jan 21, 2026

• zenon_modulo

  Public
  First-order automated theorem prover based on the tableau method

  OCaml

  •

  Other

  •7•18•3•0•Updated Jan 3, 2026Jan 3, 2026

• coq-hol-light

  Public
  Translation of HOL-Light's Multivariate library in Rocq

  lambdapihol-lightrocq-prover+ 1hol2dk

  Rocq Prover

  •

  Other

  •3•7•0•1•Updated Jan 1, 2026Jan 1, 2026

• isabelle_dedukti

  Public
  Isabelle component generating Dedukti proofs

  Scala

  •

  Other

  •7•6•2•1•Updated Dec 17, 2025Dec 17, 2025

• opam-repository

  Public
  Main public package repository for opam, the source package manager of OCaml.

  Creative Commons Zero v1.0 Universal

  •1.2k•0•0•0•Updated Dec 16, 2025Dec 16, 2025

• hol2dk

  Public
  HOL-Light to Dedukti/Lambdapi translator

  translationproofdedukti+ 3lambdapihol-lightrocq-prover

  Rocq Prover

  •

  Other

  •6•8•2•3•Updated Dec 15, 2025Dec 15, 2025

• rocq-hollight-logic-unif

  Public
  Translation in Rocq of HOL-Light's Logic library until unify using hol2dk

  lambdapihol-lightrocq-prover+ 1hol2dk

  Rocq Prover

  •

  Other

  •2•0•0•0•Updated Dec 15, 2025Dec 15, 2025

• Lean4Less

  Public
  A translation framework for eliminating definitional equalities in Lean

  Lean

  •1•14•0•0•Updated Dec 5, 2025Dec 5, 2025

• rocq-hollight-logic

  Public
  Translation of HOL-Light's Logic library in Rocq

  lambdapihol-lightrocq-prover+ 1hol2dk

  Rocq Prover

  •2•1•0•0•Updated Dec 3, 2025Dec 3, 2025

• lambdapi-zenon

  Public
  Lambdapi library for Zenon

  Answer Set Programming

  •

  Other

  •2•1•0•0•Updated Dec 2, 2025Dec 2, 2025

• coq-hol-light-real-with-N

  Public
  Translation in Coq of the HOL-Light definition of real numbers using binary natural numbers

  lambdapihol-lightrocq-prover+ 1hol2dk

  Rocq Prover

  •

  Other

  •5•2•0•1•Updated Dec 2, 2025Dec 2, 2025

• opam-lambdapi-repository

  Public
  Opam repository of Lambdapi libraries

  opam-repositorylambdapi

  Shell

  •2•1•0•0•Updated Nov 25, 2025Nov 25, 2025

• mathcomp-hollight-real-with-N

  Public
  Translation in Rocq of the HOL-Light definition of real numbers using MathComp

  lambdapihol-lightrocq-prover+ 1hol2dk

  Rocq Prover

  •

  Other

  •2•0•0•1•Updated Nov 25, 2025Nov 25, 2025

• Dedukti

  Public
  Type-checker for the λΠ-calculus modulo rewriting

  OCaml

  •

  Other

  •28•225•27•2•Updated Nov 25, 2025Nov 25, 2025

• lambdapi-logics

  Public
  Logic files for Lambdapi

  Answer Set Programming

  •

  Other

  •3•7•0•0•Updated Nov 24, 2025Nov 24, 2025

• coq-hol-light-real-with-nat

  Public
  Translation in Rocq of the HOL-Light definition of real numbers using the Rocq type nat

  lambdapihol-lightrocq-prover+ 1hol2dk

  Rocq Prover

  •

  Other

  •2•3•0•0•Updated Nov 24, 2025Nov 24, 2025

• TranslationTemplates

  Public
  OCaml

  •1•2•0•0•Updated Nov 20, 2025Nov 20, 2025

• lean2dk

  Public
  WIP translation from Lean to Dedukti

  deduktilean4

  Lean

  •

  Apache License 2.0

  •2•8•0•0•Updated Nov 18, 2025Nov 18, 2025

• Leo-III-lambdapi-lib

  Public
  Repository for the Lambdapi encodings of various inference rules and meta-theorems used in the verification of the HOL ATP Leo-III

  Answer Set Programming

  •0•0•0•0•Updated Oct 31, 2025Oct 31, 2025

• hol-light

  Public
  The HOL Light theorem prover

  OCaml

  •

  Other

  •85•0•0•0•Updated Oct 2, 2025Oct 2, 2025

• sublime-lambdapi

  Public
  Grammar of the Lambdapi language

  lambdapi

  MIT License

  •0•0•0•0•Updated Sep 11, 2025Sep 11, 2025

• CoqInE

  Public
  A Coq plugin to translate Coq proofs into Dedukti terms.

  OCaml

  •

  GNU Lesser General Public License v2.1

  •6•10•8•2•Updated Sep 4, 2025Sep 4, 2025

• pog2why

  Public
  Translate a POG file into a lambdapi file

  OCaml

  •2•3•0•0•Updated Feb 17, 2025Feb 17, 2025

• Logipedia

  Public
  An encyclopedia of proofs

  OCaml

  •12•64•7•3•Updated Nov 11, 2024Nov 11, 2024

• Construkti

  Public
  A double negation translator for higher-order Dedukti proofs

  OCaml

  •1•3•0•0•Updated Sep 20, 2024Sep 20, 2024

• dedukti.github.io

  Public
  Webpage for Dedukti

  HTML

  •4•2•1•1•Updated Sep 19, 2024Sep 19, 2024

• personoj

  Public
  People's Verification System in Dedukti

  Common Lisp

  •

  Other

  •3•6•0•1•Updated Jul 2, 2024Jul 2, 2024