25 June 2018

Program (add what you want):

• Point on the current version (2.6) of Dedukti (now on the main ocaml opam repo) and the tools generating Dedukti files. Which tools are not on Github yet? Which tools do not use CI with Travis yet?

• Discussion on the syntax of Dedukti (proposed by Rodolphe and Frédéric). The extension of Dedukti into a proof assistant requires to extend it with a tactic language. I propose to use Ssreflect. Then, it would be nice to have something uniform and more user-friendly than something like #CMD.

  • Should we completely redesign it?
  • What features in the base language? (let, ...)
  • Support for pre-processing/desugaring? (Sukerujo)
  • Definable symbols by default?
  • ...

• Polarized Dedukti (proposed by Guillaume Burel)

  • Syntax of the polarized rules (for the moment it is -->+ and -->-)
  • Merge into master ?

• Logipedia (Gilles): I have one suggestion : now that we have an online library of proofs, we should be able to reference in a Dedukti proof, a variable by its url. For instance, imagine that the page logipedia.science/pi is a proof of a theorem A and I want to prove (A /\ A). I should be able, instead of downloading the proof in my local library, to write the proof <logipedia.science/pi, logipedia.science/pi>. The proof-checker could trust Logipedia, but it should check that all free variables of pi are declared in my local context (this is the purpose of the indirect dependences / theory of the page logipedia.science/pi).