@Deducteam
Guthub

Deducteam

Twitter logo Share LinkedIn logo Share Facebook logo Share
  • Stars
    star
    618
  • Global Org. Rank 20,983 (Top 7 %)
  • Registered about 7 years ago
  • Most used languages
    OCaml
         58.6 %
    Makefile     13.8 %
    Common Lisp
         6.9 %
    Agda     3.4 %
    Lean     3.4 %
    Coq     3.4 %
    Haskell
         3.4 %
    Scala
         3.4 %
    Shell
         3.4 %

Top repositories

1

lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting
OCaml
268
star
2

Dedukti

Implementation of the λΠ-calculus modulo rewriting
OCaml
198
star
3

Logipedia

An encyclopedia of proofs
OCaml
56
star
4

Agda2Dedukti

Haskell
16
star
5

zenon_modulo

First-order automated theorem prover based on the tableau method
OCaml
11
star
6

SizeChangeTool

A termination checker for higher-order rewriting with dependent types
OCaml
9
star
7

CoqInE

A Coq plugin to translate Coq proofs into Dedukti terms.
OCaml
7
star
8

hol2dk

HOL-Light to Dedukti/Lambdapi translator
OCaml
6
star
9

predicativize

A tool for sharing proofs with predicative systems
OCaml
5
star
10

dkmeta

A tool to rewrite Dedukti terms using rewrite rules
OCaml
4
star
11

Libraries

A collection of hand-written files for Dedukti
Makefile
4
star
12

lean2dk

WIP translation from Lean to Dedukti
Lean
4
star
13

matita_lib_in_agda

Agda
3
star
14

universo

A universe reconstruction tool based on Dedukti and the encoding of CiC in Dedukti
OCaml
3
star
15

personoj

People's Verification System in Dedukti
Common Lisp
3
star
16

isabelle_dedukti

Isabelle component generating Dedukti proofs
Scala
3
star
17

lambdapi-logics

Logic files for Lambdapi
Makefile
3
star
18

coq-hol-light

HOL-Light library in Coq
Coq
3
star
19

ekstrakto

Extract TPTP problems from a TSTP trace and reconstruct the proof in lambdapi (λΠ-calculus modulo theory).
OCaml
2
star
20

lambdapi-stdlib

Repository of Lambdapi developments
Makefile
2
star
21

Holide

A translator from OpenTheory to Dedukti
OCaml
2
star
22

zenon_modulo-lib-gen

Translation script (from BWare to Dedukti) using Zenon Modulo
Shell
1
star
23

Sukerujo

Syntactic sugar for Dedukti
OCaml
1
star
24

smt2d

Translation from the SMT-LIB language to Dedukti
OCaml
1
star
25

resystance

Rewrite system stats n' count
OCaml
1
star
26

pvs-with-proofs

Common Lisp
1
star
27

dkpsuler

Instantiate constants with dkmeta
OCaml
1
star
28

nubo

Nubo is a repository of interoperable formal proofs written in Dedukti.
Makefile
1
star
29

HOLLightToDk

OCaml
1
star