Guillaume Allais

According to our database, Guillaume Allais authored at least 13 papers between 2012 and 2024.

Collaborative distances:

• Dijkstra number of five.
• Erdős number of four.

2024

Scoped and Typed Staging by Evaluation.

Guillaume Allais

Proceedings of the 2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation, 2024

2023

Seamless, Correct, and Generic Programming over Serialised Data.

Guillaume Allais

CoRR, 2023

Frex: dependently-typed algebraic simplification.

Guillaume Allais, Edwin C. Brady, Nathan Corbyn, Ohad Kammar, Jeremy Yallop

CoRR, 2023

Builtin Types Viewed as Inductive Families.

Guillaume Allais

Proceedings of the Programming Languages and Systems, 2023

Type Theory as a Language Workbench.

Jan de Muijnck-Hughes, Guillaume Allais, Edwin C. Brady

Proceedings of the Eelco Visser Commemorative Symposium, 2023

2019

POPLMark reloaded: Mechanizing proofs by logical relations.

Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, Kathrin Stark

J. Funct. Program., 2019

Generic level polymorphic n-ary functions.

Guillaume Allais

Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development, 2019

2018

A type and scope safe universe of syntaxes with binding: their semantics and proofs.

Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna

Proc. ACM Program. Lang., 2018

2017

Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic.

Guillaume Allais

Proceedings of the 23rd International Conference on Types for Proofs and Programs, 2017

Type-and-scope safe programs and their proofs.

Guillaume Allais, James Chapman, Conor McBride, James McKinna

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2014

Views of PI: Definition and computation.

Yves Bertot, Guillaume Allais

J. Formaliz. Reason., 2014

2013

New equations for neutral terms: a sound and complete decision procedure, formalized.

Guillaume Allais, Conor McBride, Pierre Boutillier

Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed programming, 2013

2012

On the Formalization of Termination Techniques based on Multiset Orderings.

René Thiemann, Guillaume Allais, Julian Nagele

Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , 2012