| Type-and-scope safe programs and their proofs G Allais, J Chapman, C McBride, J McKinna Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and …, 2017 | 54 | 2017 |
| POPLMark reloaded: Mechanizing proofs by logical relations A Abel, G Allais, A Hameer, B Pientka, A Momigliano, S Schäfer, K Stark Journal of Functional Programming 29, e19, 2019 | 43 | 2019 |
| A type and scope safe universe of syntaxes with binding: their semantics and proofs G Allais, R Atkey, J Chapman, C McBride, J McKinna Proceedings of the ACM on Programming Languages 2 (ICFP), 1-30, 2018 | 39 | 2018 |
| On the Formalization of Termination Techniques based on Multiset Orderings. R Thiemann, G Allais, J Nagele RTA, 339-354, 2012 | 29 | 2012 |
| New Equations for Neutral Terms: A Sound and Complete Decision Procedure, Formalized G Allais, P Boutillier, C McBride Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed …, 2013 | 26 | 2013 |
| Typing with leftovers: a mechanization of Intuitionistic Multiplicative-Additive Linear Logic G Allais 23rd International Conference on Types for Proofs and Programs, 1-22, 2019 | 15 | 2019 |
| A type-and scope-safe universe of syntaxes with binding: their semantics and proofs G Allais, R Atkey, J Chapman, C McBride, J McKinna Journal of Functional Programming 31, e22, 2021 | 14 | 2021 |
| agdarsec–Total Parser Combinators G Allais Journées Francophones des Langages Applicatifs 2018 JFLA 2018, 45, 0 | 7* | |
| Generic level polymorphic N-ary functions G Allais Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven …, 2019 | 5 | 2019 |
| Views of PI: Definition and computation Y Bertot, G Allais Journal of Formalized Reasoning 7 (1), 105-129, 2014 | 5 | 2014 |
| Builtin Types Viewed as Inductive Families G Allais European Symposium on Programming, 113-139, 2023 | 3 | 2023 |
| TypOS: An Operating System for Typechecking Actors G Allais, M Altenmüller, C McBride, G Nakov, FN Forsberg, C Roy 28th International Conference on Types for Proofs and Programs, 2022 | 3 | 2022 |
| Frex: dependently-typed algebraic simplification G Allais, E Brady, N Corbyn, O Kammar, J Yallop arXiv preprint arXiv:2306.15375, 2023 | 2 | 2023 |
| Forge crowbars, Acquire normal forms G Allais Technical report, University of Strathclyde, 2012. URL http://gallais. org …, 2012 | 2 | 2012 |
| Proof automatization using reflection (implementations in Agda) G Allais MSc Intern report, University of Nottingham, 2010 | 2 | 2010 |
| Type Theory as a Language Workbench J de Muijnck-Hughes, G Allais, E Brady arXiv preprint arXiv:2301.12852, 2023 | 1 | 2023 |
| Frex: indexing modulo equations with free extensions G Allais, E Brady, O Kammar, J Yallop TyDe, 2020 | 1 | 2020 |
| agdARGS-Declarative Hierarchical Command Line Interfaces G Allais TTT17, 2017 | 1 | 2017 |
| Scoped and Typed Staging by Evaluation G Allais Proceedings of the 2024 ACM SIGPLAN International Workshop on Partial …, 2024 | | 2024 |
| Seamless, Correct, and Generic Programming over Serialised Data G Allais arXiv preprint arXiv:2310.13441, 2023 | | 2023 |
Conor McBrideReader, University of Strathclyde在 strath.ac.uk 的电子邮件经过验证
