September 2022:

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

March 2023:

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

  • D3. Comparison of the approaches used in the international Software Verification competition SV-COMP and other relevant ones. [link]

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

September 2023:

  • D5. 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. [link]

  • D6. Software prototype for the automated inference of program specifications as logical axioms. [link]

  • D7. Tools for managing the dependencies between proofs, and querying and searching the database. [link]

March 2024:

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

January 2025:

  • D9. Software for translating proof formats used by automated theorem provers to Dedukti. [link]

September 2025:

  • D10. 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. [link]

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

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

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

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

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