Normalization by evaluation for typed lambda calculus with coproducts, LICS, 2001. ,
Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums, POPL, 2004. ,
Focused Natural Deduction, LPAR (Yogyakarta), 2010. ,
DOI : 10.1007/978-3-642-16242-8_12
A Systematic Approach to Canonicity in the Classical Sequent Calculus, 21st EACSL Annual Conference on Computer Science Logic, 2012. ,
Canonical sequent proofs via multi-focusing, IFIP TCS, 2008. ,
Beta-eta equality for coproducts, Proceedings of TLCA'95, number 902 in Lecture Notes in Computer Science, 1995. ,
Focusing on pattern matching, POPL, 2009. ,
Extensional rewriting with sums MS07 Dale Miller and Alexis Saurin. From proofs to focused proofs: A modular proof of focalization in linear logic, TLCA CSL, 2007. ,
Une étude logique du contrôle (appliquée à la programmation fonctionnelle et logique), 2008. ,
Structural focalization. CoRR, abs/1109, 2011. ,
The Logical Basis of Evaluation Order and Pattern-Matching, 2009. ,