{"ID":2870608,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2509.13489","arxiv_id":"2509.13489","title":"Extended Abstract: Towards a Performance Comparison of Syntax and Type-Directed NbE","abstract":"A key part of any dependent type-checker is the method for checking whether two types are equal. A common claim is that syntax-directed equality is more performant, although type-directed equality is more expressive. However, this claim is difficult to make precise, since implementations choose only one or the other approach, making a direct comparison impossible. We present some work-in-progress developing a realistic platform for direct, apples-to-apples, comparison of the two approaches, quantifying how much slower type-directed equality checking is, and analyzing why and how it can be improved.","short_abstract":"A key part of any dependent type-checker is the method for checking whether two types are equal. A common claim is that syntax-directed equality is more performant, although type-directed equality is more expressive. However, this claim is difficult to make precise, since implementations choose only one or the other ap...","url_abs":"https://arxiv.org/abs/2509.13489","url_pdf":"https://arxiv.org/pdf/2509.13489v1","authors":"[\"Chester J. F. Gould\",\"William J. Bowman\"]","published":"2025-09-16T19:41:58Z","proceeding":"cs.PL","tasks":"[\"cs.PL\"]","methods":"[]","has_code":false}