2026-07-20T05:25:17Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23367 2025-10-27T10:17:22Z ddc:004 open_access

Implementing a Type Theory with Observational Equality, Using Normalisation by Evaluation Sirman, Matthew Lennon-Bertrand, Meven Krishnaswami, Neel Dependent type theory Bidirectional typing Observational equality Normalisation by evaluation We report on an experimental implementation in Haskell of a dependent type theory featuring an observational equality type, based on Pujet et al.’s CCobs. We use normalisation by evaluation to produce an efficient normalisation function, which is used to implement a bidirectional type checker. To allow for greater expressivity, we extend the core CCobs calculus with quotient types and inductive types. To make the system usable, we explore various proof-assistant features, notably a rudimentary version of a "hole" system similar to Agda’s. While rather crude, this experience should inform other, more substantial implementation efforts of observational equality. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Matthew Sirman and Meven Lennon-Bertrand and Neel Krishnaswami 2025 Is Part Of LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2024.5 urn:nbn:de:0030-drops-233673 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.5 eng https://creativecommons.org/licenses/by/4.0/legalcode