Allais Guillaume
Allais Guillaume
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
352017
On the Formalization of Termination Techniques based on Multiset Orderings.
R Thiemann, G Allais, J Nagele
RTA, 339-354, 2012
232012
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
212018
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
152013
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
102019
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
82018
Views of PI: Definition and computation
Y Bertot, G Allais
Journal of Formalized Reasoning 7 (1), 105-129, 2014
62014
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
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
12019
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
The system can't perform the operation now. Try again later.
Articles 1–15