Deliverables
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.