Alternative implementation of the logical framework Dedukti in Rust
-
Updated
Apr 10, 2025 - Rust
#
dedukti
Here are 8 public repositories matching this topic...
HOL-Light to Dedukti/Lambdapi translator
-
Updated
Oct 27, 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
Alternative implementation of the logical framework Dedukti
-
Updated
Nov 21, 2019 - Haskell
Research-stage Julia verification toolchain for contracts, compiler analysis, numeric semantics, and verified FFI with independently checked proof targets.
open-source dependent-types compiler julia zig static-analysis memory-safety program-verification formal-verification julialang dedukti why3 research-software numerical-computing idris2 hyperpolymath epistemic-infrastructure epistemic-computing veridical-computing verified-ffi
-
Updated
Oct 29, 2026 - Shell
Research-stage verification suite for a pure OCaml subset, BEAM actor protocols, and Idris2/Zig FFI boundaries. Targets Why3/SMT, Apalache, and checked proof receipts. Current contents are architecture, an implementation roadmap, and fail-closed readiness tooling; the proof engine is not yet implemented.
distributed-systems dependent-types beam zig ocaml actor-model session-types formal-verification tla-plus dedukti why3 research-software idris2 apalache choreographic-programming hyperpolymath epistemic-computing veridical-computing verified-ffi proof-carrying-abi
-
Updated
Oct 22, 2026 - Shell
Add this topic to your repo
To associate your repository with the dedukti topic, visit your repo's landing page and select "manage topics."