  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 presents a small proof checker with support for concurrent proof checking,
achieving state-of-the-art performance in both concurrent and nonconcurrent
settings. The proof checker implements the lambda-Pi calculus modulo rewriting,
which is an established framework to uniformly express a multitude of logical
systems. The proof checker 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.
