Journal papers
- A Scope Safe Universe of Syntaxes with Binding, Their Semantics and Proofs
[ github | pdf | arXiv ]
G. Allais, R. Atkey, J. Chapman, C. McBride, J. McKinna
JFP, 2021 10
- POPLMark Reloaded: Mechanizing Proofs by Logical Relations
[ pdf ]
A. Abel, G. Allais, A. Hameer, B. Pientka, A. Momigliano, S. Schäfer, K. Stark
JFP, 2019 12
- Views of PI: Definition and computation
[ pdf ]
Y. Bertot, G. Allais
Journal of Formalized Reasoning, 2014 10
Conference papers
- Type Theory as a Language Workbench
[ github | pdf | arXiv ]
J. de Muijnck-Hughes, G. Allais, E. Brady
EVCS 2023, 2023 04
- Builtin Types viewed as Inductive Families
[ pdf | arXiv | slides ]
G. Allais
ESOP 2023, 2023 04
- A Scope Safe Universe of Syntaxes with Binding, Their Semantics and Proofs
[ github | pdf | slides ]
G. Allais, R. Atkey, J. Chapman, C. McBride, J. McKinna
PACMPL issue ICFP 2018, 2018 09
- Typing with Leftovers - A Mechanization of Intuitionistic Multiplicative Additive Linear Logic
[ github | pdf ]
G. Allais
TYPES 2017 Post Proceeding, 2018
- Type-and-Scope Safe Programs and their Proofs
[ pdf | slides | github ]
G. Allais, J. Chapman, C. McBride, J. McKinna
CPP, 2017
- On the Formalization of Termination Techniques Based on Multiset Orderings
[ pdf ]
R. Thiemann, G. Allais, J. Nagele
RTA, 2012
Workshops
- Using Dependent Types at Scale: Maintaining the Agda Standard Library
[ pdf ]
M. Daggit, G. Allais
WITS'22, 2021 11
- Frex: indexing modulo equations with free extensions
[ pdf ]
G. Allais, E. Brady, O. Kammar, J. Yallop
TyDe'20, 2020 08 03
- Generic Level Polymorphic N-ary Functions
[ github | pdf | slides | arXiv ]
G. Allais
TyDe'19, 2019 05 20
- agdarsec — Total Parser Combinators
[ github | pdf ]
G. Allais
JFLA, 2018 01
- agdARGS - Declarative Hierarchical Command Line Interfaces
[ pdf | slides | github ]
G. Allais
TTT, 2017
- New Equations for Neutral Terms: A Sound and Complete Decision Procedure, Formalized
[ pdf | arXiv ]
G. Allais, P. Boutillier, C. McBride
DTP, 2013
- Using Reflection to Solve some Differential Equations
[ pdf | slides ]
G. Allais
3rd Coq Workshop, 2011
Talks
- Seamless, Correct, and Generic Programming over Serialised Data
[ slides ]
G. Allais
SPLS, 2023 03 08
- agdarsec - Total Parser Combinators in Agda
[ github | slides ]
G. Allais
Brouwer Seminar, 2017 04 04
- Type and Scope Preserving Semantics
[ github | slides ]
G. Allais, J. Chapman, C. McBride
Scottish PL Seminar, 2015 10 21
- agdARGS - Command Line Arguments, Options and Flags
[ github | slides ]
G. Allais
Idris Developers Meeting, 2015 03 18
- Resource Aware Contexts and Proof Search for IMLL
[ github ]
G. Allais
PL Interest Seminar - University of Edinburgh, 2014 06 30
- Generic Generalised de Bruijn indices
G. Allais
Gallium Seminar - INRIA Paris-Rocquencourt, 2014 02 17
- Glueing Terms to Models: Variations on NbE
[ pdf | blog ]
G. Allais
MSP Away Day - University of Strathclyde, 2013 06 05
Drafts
- Certified Proof Search for Intuitionistic Linear Logic
[ github | pdf ]
G. Allais, C. McBride
Submitted to TLCA, 2015 02
Technical reports
- Syntaxes with Binding, Their Programs, and Proofs
[ github | pdf ]
G. Allais
PhD Thesis, 2021 06
- Forge Crowbars, Acquire Normal Forms
[ pdf | github ]
G. Allais
University of Strathclyde, 2013
- Deciding Presburger Arithmetic using Reflection
[ pdf | slides | github ]
G. Allais
ENS Lyon / University of Nottingham, 2010
Last update: 2023 07
