certification, concept alignment, dependent type theory, higher-order logic, logical frameworks, proof transformation, proof translation, rewriting.
