Repositories list

• lambdapi

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

  dependent-typesproof-assistantrewriting+ 3

  dependent-typesproof-assistantrewritingproof-checkerlogical-frameworkproof-translator

  OCaml

  •

  Other

  •4141 forks•388388 stars•9797 issues•1919 pull requests•Updated Apr 23, 2026Apr 23, 2026

• lambdapi-logics

  Public
  Logic files for Lambdapi

  Lambdapi

  •

  Other

  •33 forks•77 stars•00 issues•00 pull requests•Updated Apr 23, 2026Apr 23, 2026

• coq-hol-light

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

  lambdapihol-lightrocq-prover+ 1

  lambdapihol-lightrocq-proverhol2dk

  Rocq Prover

  •

  Other

  •44 forks•77 stars•00 issues•22 pull requests•Updated Apr 1, 2026Apr 1, 2026

• hol2dk

  Public
  HOL-Light to Dedukti/Lambdapi translator

  translationproofdedukti+ 3

  translationproofdeduktilambdapihol-lightrocq-prover

  Rocq Prover

  •

  Other

  •66 forks•88 stars•22 issues•44 pull requests•Updated Apr 1, 2026Apr 1, 2026

• rocq-hollight

  Public
  Translation of HOL-Light libraries in Rocq

  Rocq Prover

  •

  Other

  •33 forks•00 stars•00 issues•11 pull request•Updated Mar 27, 2026Mar 27, 2026

• isabelle_dedukti

  Public
  Isabelle component generating Dedukti proofs

  Scala

  •

  Other

  •77 forks•66 stars•33 issues•11 pull request•Updated Mar 12, 2026Mar 12, 2026

• eo2lp

  Public
  Tool for translating Eunoia to LambdaPi

  OCaml

  •11 fork•00 stars•00 issues•00 pull requests•Updated Feb 23, 2026Feb 23, 2026

• 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

  Lambdapi

  •00 forks•11 star•00 issues•00 pull requests•Updated Feb 20, 2026Feb 20, 2026

• Lean4Less

  Public
  A translation framework for eliminating definitional equalities in Lean

  Lean

  •11 fork•1414 stars•00 issues•00 pull requests•Updated Feb 15, 2026Feb 15, 2026

• lambdapi-stdlib

  Public
  Repository of Lambdapi developments

  lambdapi

  lambdapi

  Lambdapi

  •

  Other

  •1010 forks•77 stars•11 issue•66 pull requests•Updated Feb 2, 2026Feb 2, 2026

• zenon_modulo

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

  OCaml

  •

  Other

  •77 forks•1818 stars•33 issues•00 pull requests•Updated Jan 3, 2026Jan 3, 2026

• opam-repository

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

  Creative Commons Zero v1.0 Universal

  •1.2k1.2k forks•00 stars•00 issues•00 pull requests•Updated Dec 16, 2025Dec 16, 2025

• rocq-hollight-logic-unif

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

  lambdapihol-lightrocq-prover+ 1

  lambdapihol-lightrocq-proverhol2dk

  Rocq Prover

  •

  Other

  •22 forks•00 stars•00 issues•00 pull requests•Updated Dec 15, 2025Dec 15, 2025

• rocq-hollight-logic

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

  lambdapihol-lightrocq-prover+ 1

  lambdapihol-lightrocq-proverhol2dk

  Rocq Prover

  •22 forks•11 star•00 issues•00 pull requests•Updated Dec 3, 2025Dec 3, 2025

• lambdapi-zenon

  Public
  Lambdapi library for Zenon

  Answer Set Programming

  •

  Other

  •22 forks•11 star•00 issues•00 pull requests•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+ 1

  lambdapihol-lightrocq-proverhol2dk

  Rocq Prover

  •

  Other

  •77 forks•22 stars•00 issues•11 pull request•Updated Dec 2, 2025Dec 2, 2025

• opam-lambdapi-repository

  Public
  Opam repository of Lambdapi libraries

  opam-repositorylambdapi

  opam-repositorylambdapi

  Shell

  •44 forks•11 star•00 issues•00 pull requests•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+ 1

  lambdapihol-lightrocq-proverhol2dk

  Rocq Prover

  •

  Other

  •22 forks•00 stars•00 issues•11 pull request•Updated Nov 25, 2025Nov 25, 2025

• Dedukti

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

  OCaml

  •

  Other

  •2828 forks•232232 stars•2727 issues•22 pull requests•Updated Nov 25, 2025Nov 25, 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+ 1

  lambdapihol-lightrocq-proverhol2dk

  Rocq Prover

  •

  Other

  •22 forks•33 stars•00 issues•00 pull requests•Updated Nov 24, 2025Nov 24, 2025

• TranslationTemplates

  Public
  OCaml

  •11 fork•22 stars•00 issues•00 pull requests•Updated Nov 20, 2025Nov 20, 2025

• lean2dk

  Public
  WIP translation from Lean to Dedukti

  deduktilean4

  deduktilean4

  Lean

  •

  Apache License 2.0

  •22 forks•88 stars•00 issues•00 pull requests•Updated Nov 18, 2025Nov 18, 2025

• hol-light

  Public
  The HOL Light theorem prover

  OCaml

  •

  Other

  •9292 forks•00 stars•00 issues•00 pull requests•Updated Oct 2, 2025Oct 2, 2025

• sublime-lambdapi

  Public
  Grammar of the Lambdapi language

  lambdapi

  lambdapi

  MIT License

  •00 forks•00 stars•00 issues•00 pull requests•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

  •66 forks•1010 stars•77 issues•22 pull requests•Updated Sep 4, 2025Sep 4, 2025

• pog2why

  Public
  Translate a POG file into a lambdapi file

  OCaml

  •22 forks•33 stars•00 issues•00 pull requests•Updated Feb 17, 2025Feb 17, 2025

• Logipedia

  Public
  An encyclopedia of proofs

  OCaml

  •1212 forks•6363 stars•77 issues•33 pull requests•Updated Nov 11, 2024Nov 11, 2024

• Construkti

  Public
  A double negation translator for higher-order Dedukti proofs

  OCaml

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

• dedukti.github.io

  Public
  Webpage for Dedukti

  HTML

  •44 forks•22 stars•11 issue•11 pull request•Updated Sep 19, 2024Sep 19, 2024

• personoj

  Public
  People's Verification System in Dedukti

  Common Lisp

  •

  Other

  •33 forks•66 stars•00 issues•11 pull request•Updated Jul 2, 2024Jul 2, 2024