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