Deducteam

Pinned Repositories

Agda2Dedukti
Language:Haskell17 4 34
CoqInE
A Coq plugin to translate Coq proofs into Dedukti terms.
Language:OCaml7 4 104
Dedukti
Implementation of the λΠ-calculus modulo rewriting
Language:OCaml200 17 14022
hol2dk
HOL-Light to Dedukti/Lambdapi translator
Language:OCaml6 3 53
lambdapi
Proof assistant based on the λΠ-calculus modulo rewriting
Language:OCaml286 14 54335
lambdapi-stdlib
Repository of Lambdapi developments
Language:Makefile5 3 06
Logipedia
An encyclopedia of proofs
Language:OCaml57 12 2011
predicativize
A tool for sharing proofs with predicative systems
Language:OCaml5 2 00
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:OCaml12 6 56

Deducteam's Repositories

Deducteam/lambdapi
Proof assistant based on the λΠ-calculus modulo rewriting
Language:OCaml286 14 54335
Deducteam/Dedukti
Implementation of the λΠ-calculus modulo rewriting
Language:OCaml200 17 14022
Deducteam/Logipedia
An encyclopedia of proofs
Language:OCaml57 12 2011
Deducteam/zenon_modulo
First-order automated theorem prover based on the tableau method
Language:OCaml12 6 56
Deducteam/CoqInE
A Coq plugin to translate Coq proofs into Dedukti terms.
Language:OCaml7 4 104
Deducteam/hol2dk
HOL-Light to Dedukti/Lambdapi translator
Language:OCaml6 3 53
Deducteam/lambdapi-stdlib
Repository of Lambdapi developments
Language:Makefile5 3 06
Deducteam/lean2dk
WIP translation from Lean to Dedukti
Language:Lean4 1 01
Deducteam/coq-hol-light
HOL-Light library in Coq
Language:Coq3 4 01
Deducteam/isabelle_dedukti
Isabelle component generating Dedukti proofs
Language:Scala3 6 105
Deducteam/lambdapi-logics
Logic files for Lambdapi
Language:Makefile3 3 22
Deducteam/matita_lib_in_agda
Language:Agda3 1 0
Deducteam/personoj
People's Verification System in Dedukti
Language:Common Lisp3 3 02
Deducteam/ekstrakto
Extract TPTP problems from a TSTP trace and reconstruct the proof in lambdapi (λΠ-calculus modulo theory).
Language:OCaml2 3 73
Deducteam/nubo
Nubo is a repository of interoperable formal proofs written in Dedukti.
Language:Makefile1 3 5
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/TranslationTemplates
Language:OCaml00
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/coq-hol-light-real
Translation in Coq of the HOL-Light definition of real numbers
Language:Coq1
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/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:OCaml3 01
Deducteam/PVS
The People's Verification System
Language:Common Lisp1 0
Deducteam/sttfaxport
Language:OCaml3 02