| 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 | 35 | 2017 |
| On the Formalization of Termination Techniques based on Multiset Orderings. R Thiemann, G Allais, J Nagele RTA, 339-354, 2012 | 23 | 2012 |
| 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 | 21 | 2018 |
| 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 | 15 | 2013 |
| 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, 2019 | 10 | 2019 |
| Typing with Leftovers-A mechanization of Intuitionistic Multiplicative-Additive Linear Logic G Allais 23rd International Conference on Types for Proofs and Programs (TYPES 2017), 2018 | 8 | 2018 |
| Views of PI: Definition and computation Y Bertot, G Allais Journal of Formalized Reasoning 7 (1), 105-129, 2014 | 6 | 2014 |
| 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 |
| agdarsec–Total Parser Combinators G Allais Journées Francophones des Langages Applicatifs 2018 JFLA 2018, 45, 0 | 2* | |
| Generic level polymorphic N-ary functions G Allais Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven …, 2019 | 1 | 2019 |
| agdARGS-Declarative Hierarchical Command Line Interfaces G Allais TTT17, 2017 | | 2017 |
| Certified Proof Search for Intuitionistic Linear Logic G Allais, C McBride | | 2015 |
| Coq with power series G Allais CTP Components for Educational Software, 6, 2011 | | 2011 |
| Deciding Presburger arithmetic using reflection G Allais | | 2010 |
Conor McBrideReader, University of StrathclydeVerified email at strath.ac.uk
