Dedukti is a proof checker for the λΠ-modulo calculus, a dependently typed λ-calculus with the addition of typed rewrite rules, capable of expressing proofs in Deduction Modulo: G. Dowek, Th. Hardin, C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, 31, 2003, pp. 33-72.
Keywords for this software
References in zbMATH (referenced in 12 articles , 1 standard article )
Showing results 1 to 12 of 12.
- Cauderlier, Raphaël: Tactics and certificates in Meta Dedukti (2018)
- Ayala-Rincón, Mauricio (ed.); Muñoz, César A. (ed.): Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26--29, 2017. Proceedings (2017)
- Cauderlier, Raphaël; Dubois, Catherine: Focalize and dedukti to the rescue for proof interoperability (2017)
- Gilbert, Frédéric: Proof certificates in PVS (2017)
- Miller, Dale: Proof checking and logic programming (2017)
- Cauderlier, Raphaël; Dubois, Catherine: ML pattern-matching, recursion, and rewriting: from focalize to dedukti (2016)
- Halmagrand, Pierre: Soundly proving B method formulæ using typed sequent calculus (2016)
- Sampaio, Augusto (ed.); Wang, Farn (ed.): Theoretical aspects of computing -- ICTAC 2016. 13th international colloquium, Taipei, Taiwan, ROC, October 24--31, 2016. Proceedings (2016)
- Cauderlier, Raphaël; Dubois, Catherine: Objects and subtyping in the (\lambda)-(\Pi)-calculus modulo (2015)
- Miller, Dale: Proof checking and logic programming (2015)
- Delahaye, David; Doligez, Damien; Gilbert, Frédéric; Halmagrand, Pierre; Hermant, Olivier: Zenon modulo: when Achilles outruns the tortoise using deduction modulo (2013)
- Cousineau, Denis: On completeness of reducibility candidates as a semantics of strong normalization (2012)