Guillaume Allais

Publication Activity (10 Years)

Years Active: 2012-2024
Publications (10 Years): 16

Top Topics

Top Venues

J. Funct. Program.

Proc. ACM Program. Lang.

Publications

Guillaume Allais
Scoped and Typed Staging by Evaluation. PEPM (2024)
Guillaume Allais, Edwin C. Brady, Nathan Corbyn, Ohad Kammar, Jeremy Yallop
Frex: dependently-typed algebraic simplification. CoRR (2023)
Guillaume Allais
Builtin Types Viewed as Inductive Families. ESOP (2023)
Guillaume Allais
Seamless, Correct, and Generic Programming over Serialised Data. CoRR (2023)
Guillaume Allais
Builtin Types viewed as Inductive Families. CoRR (2023)
Jan de Muijnck-Hughes, Guillaume Allais, Edwin C. Brady
Type Theory as a Language Workbench. Eelco Visser Commemorative Symposium (2023)
Jan de Muijnck-Hughes, Guillaume Allais, Edwin C. Brady
Type Theory as a Language Workbench. CoRR (2023)
Guillaume Allais
Scoped and Typed Staging by Evaluation. CoRR (2023)
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna
A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. J. Funct. Program. 31 (2021)
Guillaume Allais
Generic Level Polymorphic N-ary Functions. CoRR (2021)
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna
A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs. CoRR (2020)
Guillaume Allais
Generic level polymorphic n-ary functions. TyDe@ICFP (2019)
Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, Kathrin Stark
POPLMark reloaded: Mechanizing proofs by logical relations. J. Funct. Program. 29 (2019)
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna
A type and scope safe universe of syntaxes with binding: their semantics and proofs. Proc. ACM Program. Lang. 2 (ICFP) (2018)
Guillaume Allais, James Chapman, Conor McBride, James McKinna
Type-and-scope safe programs and their proofs. CPP (2017)
Guillaume Allais
Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic. TYPES (2017)
Yves Bertot, Guillaume Allais
Views of PI: Definition and computation. J. Formaliz. Reason. 7 (1) (2014)
Guillaume Allais, Pierre Boutillier, Conor McBride
New Equations for Neutral Terms: A Sound and Complete Decision Procedure, Formalized CoRR (2013)
Guillaume Allais, Conor McBride, Pierre Boutillier
New equations for neutral terms: a sound and complete decision procedure, formalized. DTP@ICFP (2013)
René Thiemann, Guillaume Allais, Julian Nagele
On the Formalization of Termination Techniques based on Multiset Orderings. RTA (2012)