Thursday 2 March 2017, 9:00: Tactics and certificates in Meta Dedukti, Raphaël Cauderlier (IRIF).

Tactics are often featured in proof assistants to simplify the interactive development of proofs by allowing domain-specific automation. Moreover, tactics are also helpful to check the output of automatic provers which often omit details.
We use meta-programming to define a tactic language for Dedukti which can be used both for checking certificates produced by automatic provers and for developing Dedukti proofs interactively.
More precisely, we propose a dependently-typed tactic language for first-order logic in Meta Dedukti and an untyped certificate language built on top of the tactic language.