11 citations · 13 across the 7 of their papers we have counts for
7 papers
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…
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…
Type Theory as a Language Workbench
Jan de Muijnck-Hughes, Guillaume Allais, Edwin Brady
Language Workbenches offer language designers an expressive environment in which to create their DSLs. Similarly, research into mechanised meta-theory has shown how dependently typ…
Builtin Types viewed as Inductive Families
Guillaume Allais
State of the art optimisation passes for dependently typed languages can help erase the redundant information typical of invariant-rich data structures and programs. These automate…
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…
A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs
Guillaume Allais, Robert Atkey, James Chapman +2
Almost every programming language's syntax includes a notion of binder and corresponding bound occurrences, along with the accompanying notions of -equivalence, capture-avoiding…
New Equations for Neutral Terms: A Sound and Complete Decision Procedure, Formalized
Guillaume Allais, Pierre Boutillier, Conor McBride
The definitional equality of an intensional type theory is its test of type compatibility. Today's systems rely on ordinary evaluation semantics to compare expressions in types, fr…