An Improved System of Intersection Types for Explicit Substitutions. - Daniel J. Dougherty; Stéphane Lengrand; Pierre Lescanne (IFIP TCS, 2002)

Call-by-value, call-by-name, and strong normalization for the classical sequent calculus. - Stéphane Lengrand (WRS, 2003)

Intersection types for explicit substitutions. - Stéphane Lengrand; Pierre Lescanne; Daniel J. Dougherty; Mariangiola Dezani-Ciancaglini; Steffen van Bakel (Inf. Comput., 2004)

The Language chi: Circuits, Computations and Classical Logic. - Steffen van Bakel; Stéphane Lengrand; Pierre Lescanne (ICTCS, 2005)

Extending the Explicit Substitution Paradigm. - Delia Kesner; Stéphane Lengrand (RTA, 2005)

Strong Cut-Elimination Systems for Hudelmaier's Depth-Bounded Sequent Calculus for Implicational Logic. - Roy Dyckhoff; Delia Kesner; Stéphane Lengrand (IJCAR, 2006)

LJQ: A Strongly Focused Calculus for Intuitionistic Logic. - Roy Dyckhoff; Stéphane Lengrand (CiE, 2006)

A Sequent Calculus for Type Theory. - Stéphane Lengrand; Roy Dyckhoff; James McKinna (CSL, 2006)

The lambda-context Calculus. - Murdoch Gabbay; Stéphane Lengrand (LFMTP@CADE, 2007)

Resource operators for lambda-calculus. - Delia Kesner; Stéphane Lengrand (Inf. Comput., 2007)

Call-by-Value lambda-calculus and LJQ. - Roy Dyckhoff; Stéphane Lengrand (J. Log. Comput., 2007)

Strong Normalisation of Cut-Elimination That Simulates beta-Reduction. - Kentaro Kikuchi; Stéphane Lengrand (FoSSaCS, 2008)

Classical Fomega, orthogonality and symmetric candidates. - Stéphane Lengrand; Alexandre Miquel (Ann. Pure Appl. Log., 2008)

Termination of lambda-calculus with the extra Call-By-Value rule known as assoc - Stéphane Lengrand (CoRR, 2008)

The lambda-context calculus (extended version). - Murdoch James Gabbay; Stéphane Lengrand (Inf. Comput., 2009)

Filter Models: Non-idempotent Intersection Types, Orthogonality and Polymorphism. - Alexis Bernadet; Stéphane Lengrand (CSL, 2011)

Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types. - Alexis Bernadet; Stéphane Lengrand (FoSSaCS, 2011)

A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems - Stéphane Lengrand; Roy Dyckhoff; James McKinna (Log. Methods Comput. Sci., 2011)

A sequent calculus with procedure calls - Mahfuza Farooque; Stéphane Lengrand (CoRR, 2012)

Two simulations about DPLL(T) - Mahfuza Farooque; Stéphane Lengrand; Assia Mahboubi (CoRR, 2012)

A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus. - Mahfuza Farooque; Stéphane Graham-Lengrand; Assia Mahboubi (LFMTP, 2013)

Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture. - Stéphane Graham-Lengrand (TABLEAUX, 2013)

A simple presentation of the effective topos. - Alexis Bernadet; Stéphane Graham-Lengrand (CoRR, 2013)

Non-idempotent intersection types and strong normalisation. - Alexis Bernadet; Stéphane Lengrand (Log. Methods Comput. Sci., 2013)

Sequent Calculi with procedure calls - Mahfuza Farooque; Stéphane Graham-Lengrand (CoRR, 2013)

Polarities & Focussing: a journey from Realisability to Automated Reasoning. - Stéphane Graham-Lengrand (2014)

Polarities & Focussing: a journey from Realisability to Automated Reasoning. - Stéphane Graham-Lengrand (CoRR, 2014)

Axiomatisation of constraint systems to specify a tableaux calculus modulo theories. - Damien Rouhling; Mahfuza Farooque; Stéphane Graham-Lengrand; Assia Mahboubi; Jean-Marc Notin (CoRR, 2014)

Axiomatic Constraint Systems for Proof Search Modulo Theories. - Damien Rouhling; Mahfuza Farooque; Stéphane Graham-Lengrand; Assia Mahboubi; Jean-Marc Notin (FroCos, 2015)

Realisability semantics of abstract focussing, formalised. - Stéphane Graham-Lengrand (WoF'15, 2015)

Special Issue on Computational Logic in Honour of Roy Dyckhoff. - Didier Galmiche; Stéphane Graham-Lengrand (J. Log. Comput., 2016)

Satisfiability Modulo Theories and Assignments. - Maria Paola Bonacina; Stéphane Graham-Lengrand; Natarajan Shankar (CADE, 2017)

An MCSAT treatment of Bit-Vectors. - Stéphane Graham-Lengrand; Dejan Jovanovic (SMT, 2017)

Proofs in conflict-driven theory combination. - Maria Paola Bonacina; Stéphane Graham-Lengrand; Natarajan Shankar (CPP, 2018)

Tight typings and split bounds. - Beniamino Accattoli; Stéphane Graham-Lengrand; Delia Kesner (Proc. ACM Program. Lang., 2018)

A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic. - Camillo Fiorentini; Rajeev Goré; Stéphane Graham-Lengrand (TABLEAUX, 2019)

Solving Bitvectors with MCSAT: Explanations from Bits and Pieces. - Stéphane Graham-Lengrand; Dejan Jovanovic; Bruno Dutertre (IJCAR (1), 2020)

Solving bitvectors with MCSAT: explanations from bits and pieces (long version). - Stéphane Graham-Lengrand; Dejan Jovanovic; Bruno Dutertre (CoRR, 2020)

Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness. - Maria Paola Bonacina; Stéphane Graham-Lengrand; Natarajan Shankar (J. Autom. Reason., 2020)

Tight typings and split bounds, fully developed. - Beniamino Accattoli; Stéphane Graham-Lengrand; Delia Kesner (J. Funct. Program., 2020)

Semantic parsing of geometry statements using supervised machine learning on synthetic data. - Salwa Tabet Gonzalez; Stéphane Graham-Lengrand; Julien Narboux; Natarajan Shankar (CICM Workshops, 2021)

Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head. - José Carlos Bacelar Almeida; Manuel Barbosa; Karim Eldefrawy; Stéphane Graham-Lengrand; Hugo Pacheco 001; Vitor Pereira 002 (CoRR, 2021)

Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head. - José Bacelar Almeida; Manuel Barbosa; Manuel L. Correia; Karim Eldefrawy; Stéphane Graham-Lengrand; Hugo Pacheco 001; Vitor Pereira 002 (IACR Cryptol. ePrint Arch., 2021)

CDSAT for Nondisjoint Theories with Shared Predicates: Arrays With Abstract Length. - Maria Paola Bonacina; Stéphane Graham-Lengrand; Natarajan Shankar (SMT, 2022)

Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs. - Maria Paola Bonacina; Stéphane Graham-Lengrand; Natarajan Shankar (J. Autom. Reason., 2022)

QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment. - Maria Paola Bonacina; Stéphane Graham-Lengrand; Christophe Vauthier (CADE, 2023)

Boosting the Performance of High-Assurance Cryptography: Parallel Execution and Optimizing Memory Access in Formally-Verified Line-Point Zero-Knowledge. - Samuel Dittmer; Karim Eldefrawy; Stéphane Graham-Lengrand; Steve Lu 001; Rafail Ostrovsky; Vitor Pereira 002 (IACR Cryptol. ePrint Arch., 2023)

MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver (Short Paper). - Thomas Hader; Daniela Kaufmann; Ahmed Irfan; Stéphane Graham-Lengrand; Laura Kovács (IJCAR (1), 2024)

Arrays Reasoning in MCSat. - Ahmed Irfan; Stéphane Graham-Lengrand (SMT@CAV, 2024)

MCSat-based Finite Field Reasoning in the Yices2 SMT Solver. - Thomas Hader; Daniela Kaufmann; Ahmed Irfan; Stéphane Graham-Lengrand; Laura Kovács (CoRR, 2024)

Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search. - Enrico Lipparini; Thomas Hader; Ahmed Irfan; Stéphane Graham-Lengrand (CADE, 2025)

Decision Heuristics in MCSat. - Thomas Hader; Ahmed Irfan; Stéphane Graham-Lengrand (CAV (3), 2025)

The QSMA Algorithm for Quantifiers in SMT. - Maria Paola Bonacina; Stéphane Graham-Lengrand; Christophe Vauthier (J. Autom. Reason., 2025)