European Research Network on Formal Proofs
COST action CA20111
COST logo
EU flag and COST acknowledgement
COST (European Cooperation in Science and Technology) is a funding agency for research and innovation networks. Our Actions help connect research initiatives across Europe and enable scientists to grow their ideas by sharing them with their peers. This boosts their research, career and innovation.

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.

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.