I thought Dedukti has a small kernel. Although “small” may be a relative thing (relative to other dependently typed systems.