The aim of this WG is to investigate various approaches to efficiently maintain libraries of formal proofs. The goal is to make a collection of proofs that can be modified, extended, and queried by users who do not have expert knowledge of the entire collection nor of the system that was used to develop the proofs.

Activities

  • 24-25 June 2022: school on Dedukti and the encoding of proofs of various systems in Dedukti, and a workshop on Women in EuroProofNet, in co-location with the TYPES’22 conference at Nantes (France)

  • August 2022: workshop dedicated to sharing libraries of formal proofs during FLOC at Haifa (Israel)