2 citations · 2 across the 3 of their papers we have counts for
3 papers
cs.PL2025
Extended Abstract: Towards a Performance Comparison of Syntax and Type-Directed NbE
Chester J. F. Gould, William J. Bowman
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-d…
cs.PL2025
Fast and Extensible Hybrid Embeddings with Micros
Sean Bocirnea, William J. Bowman
Macro embedding is a popular approach to defining extensible shallow embeddings of object languages in Scheme like host languages. While macro embedding has even been shown to enab…
cs.PL2024★ 2 cited
Type Universes as Allocation Effects
Paulette Koronkevich, William J. Bowman
In this paper, we explore a connection between type universes and memory allocation. Type universe hierarchies are used in dependent type theories to ensure consistency, by forbidd…