Follow
Allais Guillaume
Allais Guillaume
Chancellor's Fellow, University of Strathclyde
Verified email at strath.ac.uk - Homepage
Title
Cited by
Cited by
Year
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
462017
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
342019
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
332018
On the Formalization of Termination Techniques based on Multiset Orderings.
R Thiemann, G Allais, J Nagele
RTA, 339-354, 2012
262012
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
212013
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
102018
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
82021
Views of PI: Definition and computation
Y Bertot, G Allais
Journal of Formalized Reasoning 7 (1), 105-129, 2014
52014
agdarsec–Total Parser Combinators
G Allais
Journées Francophones des Langages Applicatifs 2018 JFLA 2018, 45, 0
5*
Generic level polymorphic N-ary functions
G Allais
Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven …, 2019
32019
Frex: dependently-typed algebraic simplification
G ALLAIS, E Brady, N Corbyn, O Kammar, J Yallop
Draft, 2022
22022
Forge crowbars, Acquire normal forms
G Allais
Technical report, University of Strathclyde, 2012. URL http://gallais. org …, 2012
22012
Proof automatization using reflection (implementations in Agda)
G Allais
MSc Intern report, University of Nottingham, 2010
22010
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
1*2022
Frex: indexing modulo equations with free extensions
G Allais, E Brady, O Kammar, J Yallop
TyDe, 2020
12020
Type Theory as a Language Workbench
J de Muijnck-Hughes, G Allais, E Brady
arXiv preprint arXiv:2301.12852, 2023
2023
Builtin Types viewed as Inductive Families
G Allais
arXiv preprint arXiv:2301.02194, 2023
2023
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
The system can't perform the operation now. Try again later.
Articles 1–20