Implementing a Type Theory with Observational Equality, Using Normalisation by Evaluation. - Matthew Sirman; Meven Lennon-Bertrand; Neel Krishnaswami (TYPES, 2024)