3 papers
cs.HC2026
Co-Lecturing With the DED: Explaining Circuit Design via the Draw Encode Display Loop
Alasdair Lambert, Guillaume Allais, Conor Mc Bride
When representing digital circuits, 2 dimensional hand drawings free us from the linear structure of hardware description languages, enabling intuitive reasoning and making structu…
cs.PL2023
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.PL2021
Generic Level Polymorphic N-ary Functions
Guillaume Allais
Agda's standard library struggles in various places with n-ary functions and relations. It introduces congruence and substitution operators for functions of arities one and two, an…