26 citations · 45 across the 11 of their papers we have counts for
4 papers · 1 filter
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…
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…
flap: A Deterministic Parser with Fused Lexing
Jeremy Yallop, Ningning Xie, Neel Krishnaswami
Lexers and parsers are typically defined separately and connected by a token stream. This separate definition is important for modularity and reduces the potential for parsing ambi…
Defunctionalization with Dependent Types
Yulong Huang, Jeremy Yallop
The defunctionalization translation that eliminates higher-order functions from programs forms a key part of many compilers. However, defunctionalization for dependently-typed lang…