Thursday 27 September 2018, 14:00, LSV library: Rewrite tactic in Lambdapi, Aristomenis-Dionysios Papadopoulos (Intern Imperial College, London).
Aris will present the work he has done during his internship in Deducteam on the implementation of a SSReflect-like rewrite tactic in Lambdapi, the extension of Dedukti with metavariables for interactive proof development.