home
||
publications
||
teaching
||
thesis
||
blog
||
contact
2025
Type-safe Bidirectional Channels in Idris 2
[
pdf
]
G. Allais
TYPES'25
, 2025 06
Correct by Constrution Concurrent Programs in Idris 2
[
abstract
|
slides
]
G. Allais
BOB2025
, 2025 03 14
2024
Scoped and Typed Staging by Evaluation
[
pdf
|
arXiv
|
slides
]
G. Allais
PEPM 2024
, 2024 01
2023
Seamless, Correct, and Generic Programming over Serialised Data
[
pdf
|
arXiv
]
G. Allais
Submitted to POPL, 2023 07
Type Theory as a Language Workbench
[
github
|
pdf
|
arXiv
]
J. de Muijnck-Hughes
, G. Allais,
E. Brady
EVCS'23
, 2023 04
Builtin Types viewed as Inductive Families
[
pdf
|
arXiv
|
slides
]
G. Allais
ESOP'23
, 2023 04
Seamless, Correct, and Generic Programming over Serialised Data
[
slides
]
G. Allais
SPLS
, 2023 03 08
2022
TypOS: An Operating System for Typechecking Actors
[
pdf
]
G. Allais, M. Altenmüller,
C. McBride
,
F. Nordvall Forsberg
, C. Roy
TYPES'22
, 2022 01
Using Dependent Types at Scale: Maintaining the Agda Standard Library
[
pdf
]
M. Daggit, G. Allais
WITS'22
, 2022 01
2021
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
Syntaxes with Binding, Their Programs, and Proofs
[
github
|
pdf
]
G. Allais
PhD Thesis, 2021 06
2020
Frex: indexing modulo equations with free extensions
[
pdf
]
G. Allais,
E. Brady
,
O. Kammar
,
J. Yallop
TyDe'20
, 2020 08 03
2019
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
Generic Level Polymorphic N-ary Functions
[
github
|
pdf
|
slides
|
arXiv
]
G. Allais
TyDe'19, 2019 05 20
2018
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
ICFP'18
, 2018 09
agdarsec — Total Parser Combinators
[
github
|
pdf
]
G. Allais
JFLA'18
, 2018 01
Typing with Leftovers - A Mechanization of Intuitionistic Multiplicative Additive Linear Logic
[
github
|
pdf
]
G. Allais
TYPES'17 Post Proceeding, 2018
2017
agdarsec - Total Parser Combinators in Agda
[
github
|
slides
]
G. Allais
Brouwer Seminar
, 2017 04 04
Type-and-Scope Safe Programs and their Proofs
[
pdf
|
slides
|
github
]
G. Allais,
J. Chapman
,
C. McBride
, J. McKinna
CPP'17
, 2017
agdARGS - Declarative Hierarchical Command Line Interfaces
[
pdf
|
slides
|
github
]
G. Allais
TTT
, 2017
2015
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
Certified Proof Search for Intuitionistic Linear Logic
[
github
|
pdf
]
G. Allais,
C. McBride
Submitted to TLCA, 2015 02
2014
Views of PI: Definition and computation
[
pdf
]
Y. Bertot
, G. Allais
Journal of Formalized Reasoning
, 2014 10
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
2013
Glueing Terms to Models: Variations on NbE
[
pdf
|
blog
]
G. Allais
MSP Away Day - University of Strathclyde, 2013 06 05
New Equations for Neutral Terms: A Sound and Complete Decision Procedure, Formalized
[
pdf
|
arXiv
]
G. Allais,
P. Boutillier
,
C. McBride
DTP'13
, 2013
Forge Crowbars, Acquire Normal Forms
[
pdf
|
github
]
G. Allais
University of Strathclyde, 2013
2012
On the Formalization of Termination Techniques Based on Multiset Orderings
[
pdf
]
R. Thiemann
, G. Allais,
J. Nagele
RTA'12
, 2012
2011
Using Reflection to Solve some Differential Equations
[
pdf
|
slides
]
G. Allais
3rd Coq Workshop
, 2011
2010
Deciding Presburger Arithmetic using Reflection
[
pdf
|
slides
|
github
]
G. Allais
ENS Lyon / University of Nottingham, 2010
Last update: 2025 04
