  Several proof assistants, such as Isabelle or Coq, can concurrently check
multiple proofs. In contrast, the vast majority of today's small proof checkers
either does not support concurrency at all or only limited forms thereof,
restricting the efficiency of proof checking on multi-core processors. This
work shows the design of a small, memory- and thread-safe kernel that
efficiently checks proofs both concurrently and non-concurrently. This design
is implemented in a new proof checker called Kontroli for the lambda-Pi
calculus modulo rewriting, which is an established framework to uniformly
express a multitude of logical systems. Kontroli is faster than the reference
proof checker for this calculus, Dedukti, on all of five evaluated datasets
obtained from proof assistants and interactive theorem provers. Furthermore,
Kontroli reduces the time of the most time-consuming part of proof checking
using eight threads by up to 6.6x.
