Deliverables

September 2022:

• Database gathering proofs from the proof systems Coq, HOL-Light and Matita, and their translations.

  • Logipedia
  • Nubo

March 2023:

• Inventory of automated theorem provers producing proofs, description of proof formats, and inventory of checking tools for these proof formats.

  • inventory

• Comparison of the approaches used in the international Software Verification competition SV-COMP.

• Definition of a mathematical framework for modular reasoning about type theories and their extensions.

September 2023:

• Release of software for translating proofs coming from important proof systems based on type theory like Isabelle, Agda, PVS, Lean or Minlog, to Dedukti and back.

  • hol2dk: HOL-Light to Dedukti, Lambdapi and Coq
  • lambdapi: Dedukti and Lambdapi to Coq
  • isabelle_dedukti: Isabelle to Dedukti and Lambdapi
  • Personoj: PVS to Lambdapi
  • Agda2dedukti: Agda to Dedukti
  • Coqine: Coq to Dedukti
  • Holide: OpenTheory to Dedukti
  • HOLLightToDk: HOL-Light to Dedukti via OpenTheory
  • STTfaXport: Dedukti/STTfa to Coq, Lean, PVS, Matita, OpenTheory
  • Krajono: Matita to Dedukti

• Software prototype for the automated inference of program specifications as logical axioms.

• Tools for managing the dependencies between proofs, and querying and searching the database.

  • FindFacts
  • SErAPIS

March 2024:

• Detailed technical report on the evaluation of techniques for learning proof search guidance and premise selection in automated theorem provers.

January 2025:

• Software for translating proof formats used by automated theorem provers to Dedukti.

  • ZenonModulo
  • ArchSAT
  • iProverModulo
  • Ekstrakto TSTP to Lambdapi
  • Skonverto deskolemizer

September 2025:

• Release of software for translating proofs coming from important proof systems based on set theory like Mizar, Atelier B or TLAPS to Dedukti and back.

• Collection of verification challenges with summary of working recipes for verifying them.

• Technique for syntax-semantics interface for program verification with or without type systems.

• Extension of the database and associated tools to other systems like Agda, Minlog, PVS, Lean, Mizar, Atelier B, TLAPS.

• White paper on including restricted natural language proof formats to existing proof libraries.

• Prototype implementation of the mathematical framework, with basic user interface, user documentation and gallery of examples of type theories.