Thursday 24 October 2019, 14:00, LSV library: Checking HOL Proof Terms, Michael Färber (deducteam, LSV).

I will report on work in progress about the generation of HOL proof terms in Isabelle as well as their translation to the Lambda-Pi-calculus modulo.