Showing cs.PLShow all
2 papers · 1 filter
cs.PL2026
Type Theory With Erasure
Constantine Theocharis, Edwin Brady
Erasure enriches type theory with a distinction between runtime relevant and irrelevant data, allowing the compilation step to safely erase the latter. Versions of this feature are…
cs.PL2025
Custom Representations of Inductive Families
Constantine Theocharis, Edwin Brady
Inductive families provide a convenient way of programming with dependent types. Yet, when it comes to compilation, their default linked-tree runtime representations, as well as th…