The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Deducteam is very pleased to announce the availability of Dkcheck 2.7 on 
Opam.

Dkcheck is a type checker for Dedukti files (extension .dk).

Dedukti is a language implementing the λΠ-calculus modulo rewriting, a 
powerful logical framework in which one can easily represent the 
propositions/types and proofs/terms of many logical/type systems like 
first and higher-order logic, pure type systems, etc. and thus use it as 
an intermediate language for translating proofs from one system to the 
other.

There exists many tools generating Dedukti files from automated provers 
(ZenonModulo, ArchSAT, iProverModulo), TSTP files (Ekstrakto) or from 
interactive theorem provers like:

https://github.com/Deducteam/isabelle_dedukti for translating an 
Isabelle session to a Dedukti file

https://github.com/Deducteam/Agda2Dedukti for translating Agda files to 
Dedukti files

https://github.com/Deducteam/CoqInE for translating Coq files to Dedukti 
files

Conversely, there are tools generating code for Coq, Lean, PVS, 
OpenTheory or Agda from Dedukti files.

Find more details on https://deducteam.github.io/ and 
https://github.com/orgs/Deducteam/repositories.

The source code and installation instructions of Dkcheck are available 
on https://github.com/Deducteam/dedukti.

To learn more on Dedukti, you can come to the 1st Dedukti school in 
Nantes, France, on June 24-25 
(https://europroofnet.github.io/dedukti-school-2022/).

Best regards, Frédéric Blanqui, chair of https://europroofnet.github.io/.