Deducteam

Pinned Repositories

Agda2Dedukti
Language:Haskell16 4 34
CoqInE
A Coq plugin to translate Coq proofs into Dedukti terms.
Language:OCaml7 4 102
Dedukti
Implementation of the λΠ-calculus modulo rewriting
Language:OCaml196 17 13922
dkmeta
A tool to rewrite Dedukti terms using rewrite rules
Language:OCaml4 3 01
hol2dk
HOL-Light to Dedukti/Lambdapi translator
Language:OCaml6 3 53
lambdapi
Proof assistant based on the λΠ-calculus modulo rewriting
Language:OCaml268 14 51935
lean2dk
WIP translation from Lean to Dedukti
Language:Lean4 1 01
Logipedia
An encyclopedia of proofs
Language:OCaml56 10 2011
SizeChangeTool
A termination checker for higher-order rewriting with dependent types
Language:OCaml9 2 20
zenon_modulo
First-order automated theorem prover based on the tableau method
Language:OCaml11 6 56

Deducteam's Repositories

Deducteam/lambdapi
Proof assistant based on the λΠ-calculus modulo rewriting
Language:OCaml268 14 51935
Deducteam/Dedukti
Implementation of the λΠ-calculus modulo rewriting
Language:OCaml196 17 13922
Deducteam/zenon_modulo
First-order automated theorem prover based on the tableau method
Language:OCaml11 6 56
Deducteam/hol2dk
HOL-Light to Dedukti/Lambdapi translator
Language:OCaml6 3 53
Deducteam/lean2dk
WIP translation from Lean to Dedukti
Language:Lean4 1 01
Deducteam/coq-hol-light
HOL-Light library in Coq
Language:Coq31
Deducteam/isabelle_dedukti
Isabelle component generating Dedukti proofs
Language:Scala3 6 94
Deducteam/lambdapi-logics
Logic files for Lambdapi
Language:Makefile3 3 22
Deducteam/personoj
People's Verification System in Dedukti
Language:Common Lisp3 3 02
Deducteam/predicativize
A tool for sharing proofs with predicative systems
Language:OCaml3 2 00
Deducteam/ekstrakto
Extract TPTP problems from a TSTP trace and reconstruct the proof in lambdapi (λΠ-calculus modulo theory).
Language:OCaml2 3 73
Deducteam/lambdapi-stdlib
Repository of Lambdapi developments
Language:Makefile2 3 05
Deducteam/matita_lib_in_agda
Language:Agda2 1 0
Deducteam/nubo
Nubo is a repository of interoperable formal proofs written in Dedukti.
Language:Makefile1 3 5
Deducteam/smt2d
Translation from the SMT-LIB language to Dedukti
Language:OCaml1 3 0
Deducteam/Sukerujo
Syntactic sugar for Dedukti
Language:OCaml1 7 22
Deducteam/Construkti
A double negation translator for higher-order Dedukti proofs
Language:OCaml0 1 00
Deducteam/B-in-Dedukti
Implementation of the mathematical theory of the B method in Dedukti
3 0
Deducteam/cc-in-dk
Language:HTML4 0
Deducteam/Deducteam.github.io
Webpage for Dedukti and related tools
Language:HTML6 33
Deducteam/Dedukti-standard
This repository aims to provide documents which describe the Dedukti standard
Language:TeX7 6
Deducteam/hol-light
The HOL Light theorem prover
Language:OCaml0 0
Deducteam/kontroli-rs
Alternative implementation of the logical framework Dedukti in Rust
Language:Rust0 0
Deducteam/lambdapi-zenon
Lambdapi library for Zenon
Language:Makefile1
Deducteam/opam-lambdapi-repository
Opam repository of Lambdapi libraries
Language:Shell2 21
Deducteam/opam-repository
Main public package repository for opam, the source package manager of OCaml.
Language:Shell1 0
Deducteam/pog2why
Translate a POG file into a lambdapi file
Language:OCaml1
Deducteam/PVS
The People's Verification System
Language:Common Lisp1 0
Deducteam/sttfaxport
Language:OCaml3 01
Deducteam/verine
Translation of proofs from the SMT solver veriT to Dedukti
Language:OCaml3 0