Thursday 11 June 2020, 14:00, online: Minimal Concurrent Proof Checking, Michael Färber (deducteam, LSV).

Most small proof checkers, such as Dedukti, are single-threaded and thus do not exploit the potential of modern multi-core CPUs. One major obstacle for making such proof checkers multi-threaded is sharing. I present an architecture that allows for efficient proof checking in the lambda-Pi-calculus modulo both in single-threaded and multi-threaded scenarios by explicit sharing, while keeping the code size small. The resulting implementation can reduce the runtime of proof checking by up to 30%.