Translation of HOL-Light's Multivariate library in Rocq
-
Updated
Jul 1, 2026 - Rocq Prover
#
lambdapi
Here are 12 public repositories matching this topic...
HOL-Light to Dedukti/Lambdapi translator
-
Updated
Jul 24, 2026 - Rocq Prover
emdash — Functorial Type Theory (proof-assistant for ω-categories)
functional-programming coq theorem-proving proof-assistant type-theory programming-languages agda algebraic-topology isabelle algebraic-geometry coq-proof-assistant mathlib category-theory-for-programmers lambdapi edtech-software claude-code lean-prover rocq-prover codex-cli emdash
-
Updated
Sep 11, 2026 - TypeScript
Translation in Rocq of the HOL-Light definition of real numbers using the Rocq type nat
-
Updated
Jun 22, 2026 - Rocq Prover
Extract TPTP problems from a TSTP trace and reconstruct the proof in lambdapi (λΠ-calculus modulo theory).
ocaml tptp vampire automated-theorem-provers dedukti tstp lambdapi zenon-modulo e-prover zipperposition
-
Updated
Jul 6, 2021 - OCaml
Translation of HOL-Light's Logic library in Rocq
-
Updated
Jun 22, 2026 - Rocq Prover
Translation in Coq of the HOL-Light definition of real numbers using binary natural numbers
-
Updated
Sep 8, 2026 - Rocq Prover
Translation in Rocq of the HOL-Light definition of real numbers using MathComp
-
Updated
Jun 22, 2026 - Rocq Prover
Translation in Rocq of HOL-Light's Logic library until unify using hol2dk
-
Updated
Jun 22, 2026 - Rocq Prover
Add this topic to your repo
To associate your repository with the lambdapi topic, visit your repo's landing page and select "manage topics."