Summary of WG1 activities in 2023

Meetings

• 26-27 September 2023: WG1+4 meeting, Fontainebleau, France
• 25-27 July 2023: Inter-WG developers meeting, Le Val d’Ajol, France
• 11-13 May 2023: Developers meeting on proof generating automated theorem provers, Liège, Belgium
• 27-29 January 2023: 2nd Dedukti tools developers meeting, Fréjus, France

---

Publications

• Translating proofs from an impredicative type system to a predicative one (CSL’23)
• Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format (TACAS 2023)
• Bridging between LegalRuleML and TPTP for Automated Normative Reasoning (RuleML+RR 2022)
• Theorem Proving for Maude Specifications Using Lean (ICFEM’22)

---

Preprints

• A semantics of K into Dedukti
• The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography

---

New and updated translation tools

• B-pog-translator: Atelier B to lambdapi, by Clause Stolze
• lean2dk: Lean 4 to Dedukti, by Rishikesh Vaishnav
• HOL Light to Dedukti, by Frédéric Blanqui
• Personoj: PVS to lambdapi, by Gabriel Hondet
• STTfaXport: Dedukti/STTfa to Coq, Lean, PVS, Matita, OpenTheory, by Gabriel Hondet

Full list: europroofnet.github.io/deliverable5/