Dedukti : a Universal Proof Checker
Ronan Saillard, Mines Paristech · 2013
Context The success of formal methods both as tools of practical importance and as objects of intellectual curiosity, has spawned a bewildering variety of software systems to support them. While the field has developed to maturity in academia and has registered some important successes in the industry, the full benefit of formal methods in an industrial setting remains largely untapped. We submit that a lack of standards and easy interoperability in the field is one explanation to this state of affairs. The λΠ-calculus modulo To address this issue we propose the λΠ-calculus modulo as a universal proof language. This calculus, introduced by Cousineau and Dowek [5], is a dependent typed λ-calculus where the definitional equality has been generalized to an arbitrary congruence generated by rewrite rules. Our opinion is that this formalism is well suited for encoding foreign logics and make them cooperate. Indeed, by allowing the addition of user-defined rewrite rules, logics benefit from shallower encodings and do not lose their computational content.