3 papers
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
Frex: dependently-typed algebraic simplification
Guillaume Allais, Edwin Brady, Nathan Corbyn +2
We present a new design for an algebraic simplification library structured around concepts from universal algebra: theories, models, homomorphisms, and universal properties of free…
cs.PL2024
Type-level Property Based Testing
Thomas Ekström Hansen, Edwin Brady
We present an automated framework for solidifying the cohesion between software specifications, their dependently typed models, and implementation at compile time. Model Checking a…