Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Release of Dkcheck 2.7, a type-checker for Ded...


view this post on Zulip Email Gateway (Jun 18 2022 at 10:23):

From: Frédéric Blanqui <frederic.blanqui@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/.


Last updated: Jul 15 2022 at 23:21 UTC