HOL-Light to Dedukti/Lambdapi translator
-
Updated
Jul 24, 2026 - Rocq Prover
#
hol-light
Here are 11 public repositories matching this topic...
Translation of HOL-Light's Multivariate library in Rocq
-
Updated
Jul 1, 2026 - Rocq Prover
HOL-Light Library for Modal Systems
theorem-proving proof-assistant higher-order-logic interactive-theorem-proving modal-logics automated-theorem-proving hol-light
-
Updated
Jun 13, 2026 - OCaml
Translation in Rocq of the HOL-Light definition of real numbers using the Rocq type nat
-
Updated
Jun 22, 2026 - Rocq Prover
The AI mathematician that breaks conjectures before proving them, discharges every step inside a proof assistant, and hands you a proof you can check yourself.
python rust certificates coq theorem-proving proof-assistant agda isabelle formal-verification automated-reasoning cakeml metamath lean4 hol-light autoformalization ai-for-mathematics
-
Updated
Jul 21, 2026 - Rust
Translation of HOL-Light's Logic library in Rocq
-
Updated
Jun 22, 2026 - Rocq Prover
ITPEval is a benchmark suite and evaluation framework for formal statement and proof translation across Lean 4, Rocq, Isabelle/HOL, and HOL Light
-
Updated
Jul 8, 2026 - Standard ML
Translation in Coq of the HOL-Light definition of real numbers using binary natural numbers
-
Updated
Sep 8, 2026 - Rocq Prover
HOL Light Library for Modal Systems
theorem-proving proof-assistant higher-order-logic modal-logic interactive-theorem-proving automated-theorem-proving hol-light
-
Updated
Aug 30, 2026
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 hol-light topic, visit your repo's landing page and select "manage topics."