Browse by Author or creator

2025

Daggitt, Matthew L. and Allais, Guillaume and McKinna, James and Abel, Andreas and van Doorn, Nathan and Wood, James and Norell, Ulf and Kidney, Donnacha Oisín and Meshveliani, Sergei and Stucki, Sandro and Carette, Jacques and Rice, Alex and Hu, Jason Z. S. and Xia, Li-yao and You, Shu-Hung and Mullanix, Reed and Kokke, Wen (2025) The Agda standard library : version 2.0. Journal of Open Source Software, 10 (116). 9241. ISSN 2475-9066

Allais, Guillaume and Brady, Edwin and Corbyn, Nathan and Kammar, Ohad and Yallop, Jeremy (2025) Frex : dependently typed algebraic simplification. Proceedings of the ACM on Programming Languages (PACMPL), 9 (ICFP). pp. 30-65. 237. ISSN 2475-1421

2024

Allais, Guillaume (2024) Scoped and typed staging by evaluation. Other. arXiv, Ithaca, N.Y..

Allais, Guillaume; Keller, Gabriele and Wang, Meng, eds. (2024) Scoped and typed staging by evaluation. In: PEPM 2024. Association for Computing Machinery, Inc, GBR, pp. 83-93. ISBN 9798400704871

2023

Allais, Guillaume (2023) Seamless, correct, and generic programming over serialised data. Other. arXiv, Ithaca, NY.

Allais, Guillaume; Wies, Thomas, ed. (2023) Builtin types viewed as inductive families. In: Programming Languages and Systems. ESOP 2023. Lecture Notes in Computer Science, 13990 . Springer, FRA, pp. 113-139. ISBN 9783031300448

de Muijnck-Hughes, Jan and Allais, Guillaume and Brady, Edwin; Lämmel, Ralf and Mosses, Peter and Steimann, Friedrich, eds. (2023) Type theory as a language workbench. In: Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), 109 . Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl, Germany. ISBN 9783959772679

2021

Allais, Guillaume and Atkey, Robert and Chapman, James and McBride, Conor and McKinna, James (2021) A type and scope safe universe of syntaxes with binding : their semantics and proofs. Journal of Functional Programming, 31. e22. ISSN 0956-7968

2019

Allais, Guillaume; Darais, David and Gibbons, Jeremy, eds. (2019) Generic level polymorphic N-ary functions. In: TyDe 2019 - Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development, co-located with ICFP 2019. ACM, New York, NY, DEU, pp. 14-26. ISBN 9781450368155

Allais, Guillaume; Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus, eds. (2019) Typing with leftovers : a mechanization of Intuitionistic Multiplicative-Additive Linear Logic. In: 23rd International Conference on Types for Proofs and Programs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, HUN, pp. 1-22. ISBN 1868-8969

2018

Allais, Guillaume and Atkey, Robert and Chapman, James and McBride, Conor and McKinna, James (2018) A type and scope safe universe of syntaxes with binding : their semantics and proofs. Proceedings of the ACM on Programming Languages (PACMPL), 2 (ICFP). pp. 1-30. 90. ISSN 2475-1421

2017

Allais, Guillaume and Chapman, James and McBride, Conor and McKinna, James; Bertot, Yves and Vafeiadis, Viktor, eds. (2017) Type-and-scope safe programs and their proofs. In: CPP 2017. ACM, New York, NY, FRA. ISBN 9781450347051

2014

Bertot, Yves and Allais, Guillaume (2014) Views of pi : definition and computation. Journal of Formalized Reasoning, 7 (1). pp. 105-129. ISSN 1972-5787

2013

Allais, Guillaume and McBride, Conor and Boutillier, Pierre; (2013) New equations for neutral terms : a sound and complete decision procedure, formalized. In: DTP '13: Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed programming. ACM, New York, pp. 13-24. ISBN 9781450323840