Guillaume Allais

23 papers A 1B 1C 2Journal 14Unranked 5
YearRankTypeTitle / Venue / Authors
2025 J jnl
Frex: Dependently Typed Algebraic Simplification.
Proc. ACM Program. Lang.
Guillaume Allais, Edwin C. Brady, Nathan Corbyn, Ohad Kammar, Jeremy Yallop
2025 C ed.
Proceedings of the 2025 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation, PEPM 2025, Denver, CO, USA, 21 January 2025
PEPM
Guillaume Allais, Yanhong Annie Liu
2025 J jnl
The Agda standard library: version 2.0.
J. Open Source Softw.
Matthew L. Daggitt, Guillaume Allais, James McKinna, Andreas Abel, Van Doorn, Nathan, James Wood, Ulf Norell, Donnacha Oisín Kidney, Sergei Meshveliani, Sandro Stucki, Jacques Carette, Alex Rice, Jason Z. S. Hu, Li-yao Xia, Shu-Hung You, Reed Mullanix, Wen Kokke
2024 C conf
Scoped and Typed Staging by Evaluation.
PEPM
Guillaume Allais
2023 A conf
Builtin Types Viewed as Inductive Families.
ESOP
Guillaume Allais
2023 J jnl
Builtin Types viewed as Inductive Families.
CoRR
Guillaume Allais
2023 J jnl
Frex: dependently-typed algebraic simplification.
CoRR
Guillaume Allais, Edwin C. Brady, Nathan Corbyn, Ohad Kammar, Jeremy Yallop
2023 J jnl
Scoped and Typed Staging by Evaluation.
CoRR
Guillaume Allais
2023 J jnl
Seamless, Correct, and Generic Programming over Serialised Data.
CoRR
Guillaume Allais
2023 — conf
Type Theory as a Language Workbench.
Eelco Visser Commemorative Symposium
Jan de Muijnck-Hughes, Guillaume Allais, Edwin C. Brady
2023 J jnl
Type Theory as a Language Workbench.
CoRR
Jan de Muijnck-Hughes, Guillaume Allais, Edwin C. Brady
2021 J jnl
A type- and scope-safe universe of syntaxes with binding: their semantics and proofs.
J. Funct. Program.
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna
2021 J jnl
Generic Level Polymorphic N-ary Functions.
CoRR
Guillaume Allais
2020 J jnl
A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs.
CoRR
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna
2019 — conf
Generic level polymorphic n-ary functions.
TyDe@ICFP
Guillaume Allais
2019 J jnl
POPLMark reloaded: Mechanizing proofs by logical relations.
J. Funct. Program.
Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, Kathrin Stark
2018 J jnl
A type and scope safe universe of syntaxes with binding: their semantics and proofs.
Proc. ACM Program. Lang.
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna
2017 B conf
Type-and-scope safe programs and their proofs.
CPP
Guillaume Allais, James Chapman, Conor McBride, James McKinna
2017 — conf
Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic.
TYPES
Guillaume Allais
2014 J jnl
Views of PI: Definition and computation.
J. Formaliz. Reason.
Yves Bertot, Guillaume Allais
2013 J jnl
New Equations for Neutral Terms: A Sound and Complete Decision Procedure, Formalized
CoRR
Guillaume Allais, Pierre Boutillier, Conor McBride
2013 — conf
New equations for neutral terms: a sound and complete decision procedure, formalized.
DTP@ICFP
Guillaume Allais, Conor McBride, Pierre Boutillier
2012 — conf
On the Formalization of Termination Techniques based on Multiset Orderings.
RTA
René Thiemann, Guillaume Allais, Julian Nagele