| Intersection types for explicit substitutions S Lengrand, P Lescanne, D Dougherty, M Dezani-Ciancaglini, ... Information and Computation 189 (1), 17-42, 2004 | 67 | 2004 |
| Call-by-value, call-by-name, and strong normalization for the classical sequent calculus S Lengrand Electronic Notes in Theoretical Computer Science 86 (4), 714-730, 2003 | 67 | 2003 |
| Non-idempotent intersection types and strong normalisation A Bernadet, SJ Lengrand arXiv preprint arXiv:1310.1622, 2013 | 65 | 2013 |
| Resource operators for λ-calculus D Kesner, S Lengrand Information and Computation 205 (4), 419-473, 2007 | 65 | 2007 |
| The Language χ: Circuits, Computations and Classical Logic S Van Bakel, S Lengrand, P Lescanne Italian Conference on Theoretical Computer Science, 81-96, 2005 | 60 | 2005 |
| LJQ: a strongly focused calculus for intuitionistic logic R Dyckhoff, S Lengrand Conference on Computability in Europe, 173-185, 2006 | 47 | 2006 |
| Complexity of strongly normalising λ-terms via non-idempotent intersection types A Bernadet, S Lengrand International Conference on Foundations of Software Science and …, 2011 | 44 | 2011 |
| Call-by-value λ-calculus and LJQ R Dyckhoff, S Lengrand Journal of Logic and Computation 17 (6), 1109-1134, 2007 | 32 | 2007 |
| Extending the explicit substitution paradigm D Kesner, S Lengrand International Conference on Rewriting Techniques and Applications, 407-422, 2005 | 30 | 2005 |
| A focused sequent calculus framework for proof search in Pure Type Systems SJE Lengrand, R Dyckhoff, J McKinna arXiv preprint arXiv:1012.3372, 2010 | 24 | 2010 |
| Normalisation & Equivalence in Proof Theory & Type Theory SJE Lengrand University of St Andrews, 2006 | 24 | 2006 |
| Classical Fω, orthogonality and symmetric candidates S Lengrand, A Miquel Annals of pure and applied logic 153 (1-3), 3-20, 2008 | 22 | 2008 |
| Tight typings and split bounds B Accattoli, S Graham-Lengrand, D Kesner Proceedings of the ACM on Programming Languages 2 (ICFP), 1-30, 2018 | 21 | 2018 |
| Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture S Graham-Lengrand International Conference on Automated Reasoning with Analytic Tableaux and …, 2013 | 20 | 2013 |
| Satisfiability modulo theories and assignments MP Bonacina, S Graham-Lengrand, N Shankar International Conference on Automated Deduction, 42-59, 2017 | 18 | 2017 |
| The λ-context calculus MJ Gabbay, S Lengrand Electronic Notes in Theoretical Computer Science 196, 19-35, 2008 | 18 | 2008 |
| Induction principles as the foundation of the theory of normalisation: Concepts and techniques S Lengrand | 18 | 2005 |
| A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus M Farooque, S Graham-Lengrand, A Mahboubi Proceedings of the Eighth ACM SIGPLAN international workshop on Logical …, 2013 | 13 | 2013 |
| On two forms of bureaucracy in derivations K Brünnler, S Lengrand Structures and Deduction 2005, 2005 | 13 | 2005 |
| Filter models: non-idempotent intersection types, orthogonality and polymorphism A Bernadet, S Lengrand Computer Science Logic (CSL'11)-25th International Workshop/20th Annual …, 2011 | 12 | 2011 |
