2 papers
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
Unboxed data constructors -- or, how cpp decides a halting problem
Nicolas Chataing, Stephen Dolan, Gabriel Scherer +1
We propose a new language feature for ML-family languages, the ability to selectively unbox certain data constructors, so that their runtime representation gets compiled away to ju…