Non-idempotent intersection types and strong normalisation A Bernadet, SJ Lengrand Logical Methods in Computer Science 9, 2013 | 77 | 2013 |

Resource operators for λ-calculus D Kesner, S Lengrand Information and Computation 205 (4), 419-473, 2007 | 73 | 2007 |

Intersection types for explicit substitutions S Lengrand, P Lescanne, D Dougherty, M Dezani-Ciancaglini, ... Information and Computation 189 (1), 17-42, 2004 | 71 | 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 | 69 | 2003 |

The Language *χ*: Circuits, Computations and Classical Logic:S Van Bakel, S Lengrand, P Lescanne Theoretical Computer Science: 9th Italian Conference, ICTCS 2005, Siena …, 2005 | 62 | 2005 |

LJQ: a strongly focused calculus for intuitionistic logic R Dyckhoff, S Lengrand Logical Approaches to Computational Barriers: Second Conference on …, 2006 | 56 | 2006 |

Call-by-value λ-calculus and LJQ R Dyckhoff, S Lengrand Journal of Logic and Computation 17 (6), 1109-1134, 2007 | 43 | 2007 |

Complexity of Strongly Normalising *λ*-Terms via Non-idempotent Intersection TypesA Bernadet, S Lengrand Foundations of Software Science and Computational Structures: 14th …, 2011 | 42 | 2011 |

Extending the explicit substitution paradigm D Kesner, S Lengrand International Conference on Rewriting Techniques and Applications, 407-422, 2005 | 37 | 2005 |

Satisfiability modulo theories and assignments MP Bonacina, S Graham-Lengrand, N Shankar Automated Deduction–CADE 26: 26th International Conference on Automated …, 2017 | 30 | 2017 |

Tight typings and split bounds B Accattoli, S Graham-Lengrand, D Kesner Proceedings of the ACM on Programming Languages 2 (ICFP), 1-30, 2018 | 29 | 2018 |

Tight typings and split bounds, fully developed B Accattoli, S Graham-Lengrand, D Kesner Journal of Functional Programming 30, e14, 2020 | 28 | 2020 |

A focused sequent calculus framework for proof search in Pure Type Systems SJE Lengrand, R Dyckhoff, J McKinna Logical Methods in Computer Science 7, 2011 | 27 | 2011 |

Normalisation & Equivalence in Proof Theory & Type Theory SJE Lengrand University of St Andrews, 2006 | 25 | 2006 |

Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture S Graham-Lengrand Automated Reasoning with Analytic Tableaux and Related Methods: 22nd …, 2013 | 23 | 2013 |

Classical Fω, orthogonality and symmetric candidates S Lengrand, A Miquel Annals of pure and applied logic 153 (1-3), 3-20, 2008 | 22 | 2008 |

The λ-context calculus MJ Gabbay, S Lengrand Electronic Notes in Theoretical Computer Science 196, 19-35, 2008 | 19 | 2008 |

Induction principles as the foundation of the theory of normalisation: Concepts and techniques S Lengrand | 18 | 2005 |

Conflict-driven satisfiability for theory combination: transition system and completeness MP Bonacina, S Graham-Lengrand, N Shankar Journal of Automated Reasoning 64 (3), 579-609, 2020 | 15 | 2020 |

A bisimulation between DPLL(*T*) and a proof-search strategy for the focused sequent calculusM Farooque, S Graham-Lengrand, A Mahboubi Proceedings of the Eighth ACM SIGPLAN international workshop on Logical …, 2013 | 14 | 2013 |