What does it take to certify a conversion checker?

TL;DR

This paper investigates the properties necessary for certifying conversion checkers in dependent type theory, emphasizing injectivity properties over normalization, and explores certification for both typed and untyped conversion checkers.

Contribution

It identifies injectivity properties as crucial and sufficient for certifying conversion checkers, and extends the certification approach to untyped conversion checkers within a typed framework.

Findings

Injectivity properties are key to certifying conversion checkers.

Certification methods extend from typed to untyped conversion checkers with subtle differences.

Normalisation is less emphasized compared to injectivity in certification.

Abstract

We report on a detailed exploration of the properties of conversion (definitional equality) in dependent type theory, with the goal of certifying decision procedures for it. While in that context the property of normalisation has attracted the most light, we instead emphasize the importance of injectivity properties, showing that they alone are both crucial and sufficient to certify most desirable properties of conversion checkers. We also explore the certification of a fully untyped conversion checker, with respect to a typed specification, and show that the story is mostly unchanged, although the exact injectivity properties needed are subtly different.