Följ
Allais Guillaume
Allais Guillaume
Verifierad e-postadress på st-andrews.ac.uk - Startsida
Titel
Citeras av
Citeras av
År
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
432017
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
312018
On the Formalization of Termination Techniques based on Multiset Orderings.
R Thiemann, G Allais, J Nagele
RTA, 339-354, 2012
282012
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
272019
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
202013
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
Views of PI: Definition and computation
Y Bertot, G Allais
Journal of Formalized Reasoning 7 (1), 105-129, 2014
62014
agdarsec–Total Parser Combinators
G Allais
Journées Francophones des Langages Applicatifs 2018 JFLA 2018, 45, 0
6*
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, 2021
52021
Generic level polymorphic N-ary functions
G Allais
Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven …, 2019
32019
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
Frex: dependently-typed algebraic simplification
G ALLAIS, E BRADY, N CORBYN, O KAMMAR, J YALLOP
2
Frex: indexing modulo equations with free extensions
G Allais, E Brady, O Kammar, J Yallop
TyDe, 2020
12020
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
TypOS: An Operating System for Typechecking Actors
G Allais, M Altenmüller, C McBride, G Nakov, FN Forsberg, C Roy
Systemet kan inte utföra åtgärden just nu. Försök igen senare.
Artiklar 1–19