What does it take to certify a conversion checker?
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866915403588960256 |
|---|---|
| author | Lennon-Bertrand, Meven |
| author_facet | Lennon-Bertrand, Meven |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_15500 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | What does it take to certify a conversion checker? Lennon-Bertrand, Meven Programming Languages Logic in Computer Science D.3.1; F.3.2; F.3.3; F.4.1 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. |
| title | What does it take to certify a conversion checker? |
| topic | Programming Languages Logic in Computer Science D.3.1; F.3.2; F.3.3; F.4.1 |
| url | https://arxiv.org/abs/2502.15500 |