Guillaume Allais

View Scopus Profile

Emailguillaume.allaisstrath.acuk

United Kingdom

Accepting PhD Students

External positions

Research Fellow, University of St Andrews

1 Apr 2020 → 31 Mar 2023

Postdoc, Radboud Universiteit Nijmegen

2016 → 2018

Fingerprint

Dive into the research topics where Guillaume Allais is active. These topic labels come from the works of this person. Together they form a unique fingerprint.

1 Similar Profiles

9 Conference contribution book
4 Article
2 Working Paper/Preprint
1 Paper
More
- 1 Conference Contribution
- 1 Conference article

The Agda standard library: version 2.0
Daggitt, M. L., Allais, G., McKinna, J., Abel, A., van Doorn, N., Wood, J., Norell, U., Kidney, D. O., Meshveliani, S., Stucki, S., Carette, J., Rice, A., Hu, J. Z. S., Xia, L.-Y., You, S.-H., Mullanix, R. & Kokke, W., 20 Dec 2025, In: Journal of Open Source Software. 10, 116, 4 p., 9241.
Research output: Contribution to journal › Article › peer-review

Open Access
File
Frex: dependently typed algebraic simplification
Allais, G., Brady, E., Corbyn, N., Kammar, O. & Yallop, J., 5 Aug 2025, In: Proceedings of the ACM on Programming Languages (PACMPL). 9, ICFP, p. 30-65 36 p., 237.
Research output: Contribution to journal › Conference article › peer-review

Open Access
File
9 Downloads (Pure)

Code for: "A type and scope safe universe of syntaxes with binding: their semantics and proofs"
Allais, G. (Creator), Atkey, R. (Creator), Chapman, J. (Creator), McBride, C. (Creator) & McKinna, J. (Creator), Association for Computing Machinery (ACM), 23 Aug 2018
DOI: 10.1145/3235048, https://github.com/gallais/generic-syntax
Dataset
Type-and-Scope Safe Programs and Their Proofs - Formalization
Chapman, J. (Creator), McBride, C. (Creator), Allais, G. (Creator) & McKinna, J. (Creator), University of Strathclyde, 9 Dec 2016
DOI: 10.15129/f1283dbb-64fd-4d35-aacc-49d3cc0893b8, https://github.com/agda/agda and one more link, https://github.com/gallais/type-scope-semantics (show fewer)
Dataset

Syntaxes with binding, their programs, and proofs
Allais, G. (Author), McBride, C. (Supervisor) & Ghani, N. (Supervisor), 12 Apr 2023
Student thesis: Doctoral Thesis

5 Invited talk
4 Organiser of special symposia
4 Oral presentation
3 Organiser of major conference
More

ICFP 2025 - ACM SIGPLAN International Conference on Functional Programming
Allais, G. (Member of programme committee)
12 Oct 2025 → 18 Oct 2025
Activity: Presenting or Organising an Event › Organiser of major conference
Type-safe Bidirectional Channels in Idris 2
Allais, G. (Speaker)
9 Jun 2025 → 13 Jun 2025
Activity: Talk or Presentation › Oral presentation

Guillaume Allais

Personal profile

External positions

Fingerprint

Collaborations and top research areas from the last five years

Dive into details

The Agda standard library: version 2.0

Frex: dependently typed algebraic simplification

Code for: "A type and scope safe universe of syntaxes with binding: their semantics and proofs"

Type-and-Scope Safe Programs and Their Proofs - Formalization

Syntaxes with binding, their programs, and proofs

ICFP 2025 - ACM SIGPLAN International Conference on Functional Programming

Type-safe Bidirectional Channels in Idris 2

Guillaume Allais

Personal profile

External positions

Fingerprint

Collaborations and top research areas from the last five years

Research output

The Agda standard library: version 2.0

Frex: dependently typed algebraic simplification

Datasets

Code for: "A type and scope safe universe of syntaxes with binding: their semantics and proofs"

Type-and-Scope Safe Programs and Their Proofs - Formalization

Thesis

Syntaxes with binding, their programs, and proofs

Activities

ICFP 2025 - ACM SIGPLAN International Conference on Functional Programming

Type-safe Bidirectional Channels in Idris 2