On the Formalization of Termination Techniques based on Multiset Orderings. - René Thiemann; Guillaume Allais; Julian Nagele (RTA, 2012)

New equations for neutral terms: a sound and complete decision procedure, formalized. - Guillaume Allais; Conor McBride; Pierre Boutillier (DTP@ICFP, 2013)

Views of PI: Definition and computation. - Yves Bertot; Guillaume Allais (J. Formaliz. Reason., 2014)

Type-and-scope safe programs and their proofs. - Guillaume Allais; James Chapman 001; Conor McBride; James McKinna (CPP, 2017)

Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic. - Guillaume Allais (TYPES, 2017)

A type and scope safe universe of syntaxes with binding: their semantics and proofs. - Guillaume Allais; Robert Atkey; James Chapman 001; Conor McBride; James McKinna (Proc. ACM Program. Lang., 2018)

Generic level polymorphic n-ary functions. - Guillaume Allais (TyDe@ICFP, 2019)

POPLMark reloaded: Mechanizing proofs by logical relations. - Andreas Abel 001; Guillaume Allais; Aliya Hameer; Brigitte Pientka; Alberto Momigliano; Steven Schäfer; Kathrin Stark (J. Funct. Program., 2019)

Type Theory as a Language Workbench. - Jan de Muijnck-Hughes; Guillaume Allais; Edwin C. Brady (Eelco Visser Commemorative Symposium, 2023)

Builtin Types Viewed as Inductive Families. - Guillaume Allais (ESOP, 2023)

Frex: dependently-typed algebraic simplification. - Guillaume Allais; Edwin C. Brady; Nathan Corbyn; Ohad Kammar; Jeremy Yallop (CoRR, 2023)

Seamless, Correct, and Generic Programming over Serialised Data. - Guillaume Allais (CoRR, 2023)

Scoped and Typed Staging by Evaluation. - Guillaume Allais (PEPM, 2024)