WG1 Tools on Proof Systems Interoperability

The aim of this WG is to coordinate the activities of the Action for developing the basic theoretical foundations and tools for the interoperability of proof systems by expressing more proof systems in the Dedukti logical framework and by developing tools to translate proofs from one system to another.

Activities

• 11-13 February 2025: WG1 meeting, Nogent-sur-Seine, France

• 26-27 September 2024: WG1+2+4 meeting, Fontainebleau, France

• 23-25 January 2024: WG1 meeting, Gruissan, France

• 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

• 16-18 October 2022: 1st Dedukti tools developers meeting, Val d’Ajol, France

• 24-25 June 2022: 1st Dedukti school at Nantes, France, colocated with TYPES’22 and Women in EuroProofNet

Grants

• From Dedukti to MMT: A Comparative Study of Modular Frameworks for Logical System application
  Visitor: Ciarán Dunne
  Host: Michael Kohlhase
  Grant: 1124 EUR
  Dates: 2025-03-10 to 2025-03-21

• Adding Extensionality to Lean application
  Visitor: Rishikesh Vaishnav
  Host: Sebastian Ullrich
  Grant: 1576 EUR
  Dates: 2025-02-17 to 2025-03-02

• Translation templates for Dedukti application report
  Visitor: Thomas Traversie
  Host: Florian Rabe
  Grant: 1530 EUR
  Dates: 2025-02-02 to 2025-02-14

• Interoperability of Tableaux and Sequent Calculus Proof Systems application report
  Visitor: Simon Guilloud
  Host: Philipp Rümmer
  Grant: 2500 EUR
  Dates: 2024-03-25 to 2024-04-06

• Translating from Lean to Dedukti application report
  Visitor: Rishikesh Vaishnav
  Host: Sebastian Ullrich
  Grant: 1500 EUR
  Dates: 2024-02-19 to 2024-02-25

• Translation of HOL4 proofs to Dedukti and Lambdapi application report
  Visitor: Frédéric Blanqui
  Host: Magnus Myreen
  Grant: 1421 EUR
  Dates: 2023-05-22 to 2023-05-26

• Translation from Dedukti to Minlog application report
  Visitor: Yoan Géran (MINES ParisTech, Fontainebleau, France)
  Host: Helmut Schwichtenberg (Mathematisches Institut der Universität München, Germany)
  Grant: 1478 EUR
  Dates: 2023-02-05 to 2023-02-12

• Automated Translation of Mizar Declarative Proof application report
  Visitor: Karol Pak (Institute of Computer Science, Bialystok, Poland)
  Host: Cezary Kaliszyk (University of Innsbruck, Austria)
  Grant: 2922 EUR
  Dates: 2023-04-17 to 2023-05-06

• Translation of Generic Symbolic Execution Steps into Dedukti application report
  Visitor: Dorel Lucanu (Alexandru Ioan Cuza University, Romania)
  Host: Gilles Dowek (Ecole Normale Superieure Paris-Saclay, France)
  Grant: 1835 EUR
  Dates: 2023-03-20 to 2023-04-01

• Leveraging a λProlog engine for type class resolution in Coq and Lambdapi application report
  Visitor: Matteo Manighetti (INRIA Saclay, Palaiseau, FR)
  Host: Enrico Tassi (Inria Université Côte d’Azur, Valbonne , FR)
  Grant: 1700 EUR
  Dates: 2022-10-15 to 2022-10-29

• Rechecking KProver proof objects into Dedukti application report
  Visitor: Amelie Ledein (Inria Saclay, Palaiseau, FR)
  Hosts: Traian Serbanuta and Dorel Lucanu (University of Bucharest, RO)
  Grant: 1520 EUR
  Dates: 2022-07-04 to 2022-07-17

• Compiling dependent pattern matching to elimination principles in Dedukti application report
  Visitor: Thiago Felicissimo (Faculté des Sciences d’Orsay, FR)
  Host: Jesper Cockx (TU Delft, NL)
  Grant: 1500 EUR
  Dates: 2022-05-08 to 2022-05-21