Deliverables
September 2022:
-
Database gathering proofs from the proof systems Coq, HOL-Light and Matita, and their translations.
March 2023:
-
Inventory of automated theorem provers producing proofs, description of proof formats, and inventory of checking tools for these proof formats.
-
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.
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.