On July 15, 2022 at 17:00 EEST, Amélie Ledein (INRIA: LMF, Deducteam) will give a talk in the Logic Seminar.
Title: Dedukti, a standard language for the interoperability of proof systems
Abstract: Dedukti is a logical framework to encode various logics to allow interoperability of proofs between different formal tools, like Coq, PVS or Isabelle. This logical framework is based on λΠ-calculus modulo theory, a λ-calculus with dependent types, and extended with rewriting rules.
After a presentation of the λΠ-calculus modulo theory, I will talk about translations to Dedukti, as well as interoperability challenges.
Finally, I will mention other work done by Deducteam.
The talk will take place at the Runtime Verification Bucharest headquarters (Popa Tatu 18); it will also be transmitted online as usual.
Google Meet link: https://meet.google.com/jps-xnmf-yoi