# Senior Computer Scientist at SRI InternationalComputer Science LaboratoryFormal Methods group

## Journal papers

 [BGLS21] M. P. Bonacina, S. Graham-Lengrand, and N. Shankar. Conflict-driven satisfiability for theory combination: Lemmas, modules, and proofs. Journal of Automated Reasoning, 2021. [ bib | DOI | .pdf ] (Subsumes Proofs in Conflict-Driven Theory Combination) [AGLK20] B. Accattoli, S. Graham-Lengrand, and D. Kesner. Tight typings and split bounds, fully developed. Journal of Functional Programming, 30:e14, 2020. [ bib | DOI | http | .pdf ] (Subsumes Tight Typings and Split Bounds and Tight Typings and Split Bounds - Long Version) [BGLS19] M. P. Bonacina, S. Graham-Lengrand, and N. Shankar. Conflict-driven satisfiability for theory combination: Transition system and completeness. Journal of Automated Reasoning, 64(3):579--609, 2019. [ bib | DOI | .pdf ] (Subsumes Satisfiability Modulo Theories and Assignments) [BGL13] A. Bernadet and S. Graham-Lengrand. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science, 9(4), 2013. [ bib | DOI | http | .pdf ] (Subsumes Complexity of strongly normalising $\lambda$-terms via non-idempotent intersection types and Filter models: non-idempotent intersection types, orthogonality and polymorphism) [LDM11] S. Lengrand, R. Dyckhoff, and J. McKinna. A focused sequent calculus framework for proof search in Pure Type Systems. Logical Methods in Computer Science, 7(1), 2011. [ bib | .pdf ] (Subsumes A sequent calculus for Type Theory) [GL09] M. Gabbay and S. Lengrand. The λ-context calculus. Information and Computation, 207(12):1369--1400, 2009. [ bib ] (Subsumes The lambda-context calculus) [LM08] S. Lengrand and A. Miquel. Classical Fω, orthogonality and symmetric candidates. Annals of Pure and Applied Logic, 153:3--20, 2008. [ bib | .pdf ] (Subsumes A classical version of Fomega) [DL07] R. Dyckhoff and S. Lengrand. Call-by-value λ-calculus and LJQ. Journal of Logic and Computation, 17:1109--1134, 2007. [ bib | DOI | .pdf ] The proof of strong normalisation of LJQ: [pdf] (updated in December 2007) [KL07] D. Kesner and S. Lengrand. Resource operators for the λ-calculus. Information and Computation, 205:419--473, 2007. [ bib | .pdf ] (Subsumes Extending the Explicit Substitution Paradigm) [LLD+04] S. Lengrand, P. Lescanne, D. Dougherty, M. Dezani-Ciancaglini, and S. van Bakel. Intersection types for explicit substitutions. Information and Computation, 189(1):17--42, 2004. [ bib | .pdf ] (Subsumes An improved system of intersection types for explicit substitutions)

## Reviewed Conference and Workshop papers

 [GLJD20] S. Graham-Lengrand, D. Jovanović, and B. Dutertre. Solving bitvectors with MCSAT: explanations from bits and pieces. In N. Peltier and V. Sofronie-Stokkermans, editors, Proceedings of the 10th International Joint Conference on Automated Reasoning (IJCAR'20), volume 12166(1) of Lecture Notes in Computer Science, pages 103--121. Springer-Verlag, January 2020. [ bib | .pdf ] (Subsumes An MCSAT treatment of Bit-Vectors and Interpolating bit-vector arithmetic constraints in MCSAT) [video] [slides] [FGGL19] C. Fiorentini, R. Goré, and S. Graham-Lengrand. A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic. In A. Popescu and S. Cerrito, editors, Proceedings of the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux'19), volume 11714 of Lecture Notes in Artificial Intelligence. Springer-Verlag, September 2019. [ bib | .pdf ] Slides: [pdf] [GLJ19] S. Graham-Lengrand and D. Jovanović. Interpolating bit-vector arithmetic constraints in MCSAT. In N. Sharygina and J. Hendrix, editors, 17th International Workshop on Satisfiability Modulo Theories (SMT 2019), July 2019. [ bib | .pdf ] Slides: [pdf] [BGLMB18] F. Bobot, S. Graham-Lengrand, B. Marre, and G. Bury. Centralizing equality reasoning in MCSAT. In R. Dimitrova and V. D'Silva, editors, 16th International Workshop on Satisfiability Modulo Theories (SMT 2018), July 2018. [ bib ] [AGLK18] B. Accattoli, S. Graham-Lengrand, and D. Kesner. Tight typings and split bounds. In M. Flatt, editor, Proceedings of the 23rd ACM International Conference on Functional Programming. ACM Press, 2018. [ bib | .pdf ] [GLF18] S. Graham-Lengrand and M. Färber. Guiding SMT solvers with Monte Carlo Tree Search and neural networks. In T. C. Hales, C. Kaliszyk, S. Schulz, and J. Urban, editors, Third Conference on Artificial Intelligence and Theorem Proving (AITP'2018), March 2018. [ bib ] [video] [BGLS18] M. P. Bonacina, S. Graham-Lengrand, and N. Shankar. Proofs in conflict-driven theory combination. In J. Andronick and A. Felty, editors, Proceedings of the 7th International Conference on Certified Programs and Proofs (CPP'18), pages 186--200. ACM Press, January 2018. [ bib | DOI | http | .pdf ] Slides: [pdf] (Subsumed by Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs) [GLJ17] S. Graham-Lengrand and D. Jovanović. An MCSAT treatment of bit-vectors. In M. Brain and L. Hadarean, editors, 15th International Workshop on Satisfiability Modulo Theories (SMT 2017), July 2017. [ bib | .pdf ] Slides: [pdf] [BGLS17] M. P. Bonacina, S. Graham-Lengrand, and N. Shankar. Satisfiability modulo theories and assignments. In L. de Moura, editor, Proceedings of the 26th International Conference on Automated Deduction (CADE'17), volume 10395 of Lecture Notes in Artificial Intelligence. Springer-Verlag, August 2017. [ bib | .pdf ] Slides: [pdf] (Subsumed by Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness) [GL15] S. Graham-Lengrand. Realisability semantics of abstract focussing, formalised. In I. Cervesato and C. Schürmann, editors, Proceedings of the the First International Workshop on Focusing, volume 197 of Electronic Proceedings in Theoretical Computer Science, pages 15--28. Open Publishing Association, November 2015. [ bib | DOI ] [RFGL+15] D. Rouhling, M. Farooque, S. Graham-Lengrand, A. Mahboubi, and J.-M. Notin. Axiomatic constraint systems for proof search modulo theories. In C. Lutz and S. Ranise, editors, Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS'15), volume 9322 of Lecture Notes in Artificial Intelligence. Springer-Verlag, September 2015. [ bib | .pdf ] Slides: [pdf] [GL13] S. Graham-Lengrand. Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture. In D. Galmiche and D. Larchey-Wendling, editors, Proceedings of the 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux'13), volume 8123 of Lecture Notes in Computer Science, pages 149--156. Springer-Verlag, September 2013. [ bib | .pdf ] Slides: [pdf] [FGLM13] M. Farooque, S. Graham-Lengrand, and A. Mahboubi. A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus. In A. Momigliano, B. Pientka, and R. Pollack, editors, Proceedings of the 2013 International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2013). ACM Press, September 2013. [ bib | DOI | .pdf ] [BL11b] A. Bernadet and S. Lengrand. Filter models: non-idempotent intersection types, orthogonality and polymorphism. In M. Bezem, editor, Proceedings of the 20th Annual Conference of the European Association for Computer Science Logic (CSL'11), Leibniz International Proceedings in Informatics. Schloss Dagstuhl Leibniz Center for Informatics, September 2011. [ bib | .pdf ] [BL11a] A. Bernadet and S. Lengrand. Complexity of strongly normalising λ-terms via non-idempotent intersection types. In M. Hofmann, editor, Proceedings of the 14th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'11), volume 6604 of Lecture Notes in Computer Science. Springer-Verlag, March 2011. [ bib | .pdf ] [KL08] K. Kikuchi and S. Lengrand. Strong normalisation of cut-elimination that simulates β-reduction. In R. Amadio, editor, Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'08), volume 4962 of Lecture Notes in Computer Science, pages 380--394. Springer-Verlag, March 2008. [ bib | .pdf ] Long version: [pdf] [GL08] M. Gabbay and S. Lengrand. The lambda-context calculus. volume 196 of Electronic Notes in Theoretical Computer Science, pages 19--35, 2008. Revision from the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2007) (was A(nother) NEW Calculus of Contexts). [ bib | DOI | .pdf ] (Subsumed by The lambda-context Calculus) [LDM06] S. Lengrand, R. Dyckhoff, and J. McKinna. A sequent calculus for type theory. In Z. Esik, editor, Proceedings of the 15th Annual Conference of the European Association for Computer Science Logic (CSL'06), volume 4207 of Lecture Notes in Computer Science, pages 441--455. Springer-Verlag, September 2006. [ bib | .pdf ] (Subsumed by A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems) [DKL06] R. Dyckhoff, D. Kesner, and S. Lengrand. Strong cut-elimination systems for Hudelmaier's depth-bounded sequent calculus for implicational logic. In U. Furbach and N. Shankar, editors, Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR'06), volume 4130 of Lecture Notes in Artificial Intelligence, pages 347--361. Springer-Verlag, August 2006. [ bib | .pdf ] Long version: [pdf] [DL06] R. Dyckhoff and S. Lengrand. LJQ, a strongly focused calculus for intuitionistic logic. In A. Beckmann, U. Berger, B. Loewe, and J. V. Tucker, editors, Proceedings of the 2nd Conference on Computability in Europe (CiE'06), volume 3988 of Lecture Notes in Computer Science, pages 173--185. Springer-Verlag, July 2006. [ bib | .pdf ] The proof of strong normalisation of LJQ: [pdf] (updated in December 2007) [LM06] S. Lengrand and A. Miquel. A classical version of Fω. In S. van Bakel and S. Berardi, editors, 1st Workshop on Classical logic and Computation, July 2006. [ bib | .pdf ] (Subsumed by Classical Fomega, orthogonality and symmetric candidates) [BL05] K. Brünnler and S. Lengrand. On two forms of bureaucracy in derivations. In F. L. Paola Bruscoli and J. Stewart, editors, 1st Workshop on Structures and Deductions (SD'05), Technical Report, Technische Universität Dresden, pages 69--80, July 2005. ISSN 1430-211X. [ bib | .pdf ] Slides [postscript] [KL05] D. Kesner and S. Lengrand. Extending the explicit substitution paradigm. In J. Giesl, editor, Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA'05), volume 3467 of Lecture Notes in Computer Science, pages 407--422. Springer-Verlag, April 2005. [ bib ] [postscript] (Best paper award RTA 2005) (Subsumed by Resource operators for the lambda-calculus) [Len04] S. Lengrand. Deriving strong normalisation. In D. Kesner, F. van Raamsdonk, and J. Wells, editors, 2nd International Workshop on Higher-Order Rewriting (HOR'04), Technical Report AIB-2004-03, RWTH Aachen, pages 84--88, June 2004. [ bib ] [postscript] (Subsumed by Induction principles as the foundation of the theory of normalisation: concepts and techniques) [Len03] S. Lengrand. Call-by-value, call-by-name, and strong normalization for the classical sequent calculus. volume 86(4) of Electronic Notes in Theoretical Computer Science. Elsevier, 2003. Revision from the 3rd International Workshop on Reduction Strategies in Rewriting and Programming (WRS'03). [ bib ] [postscript] Slides: [postscript] Erratum: [postscript] [DLL02] D. J. Dougherty, S. Lengrand, and P. Lescanne. An improved system of intersection types for explicit substitutions. In R. A. Baeza-Yates, U. Montanari, and N. Santoro, editors, Proceedings of the IFIP 17th World Computer Congress - TC1 Stream / 2nd IFIP International Conference on Theoretical Computer Science (TCS'02), volume 223 of IFIP Conference Proceedings, pages 511--523. Kluwer, August 2002. [ bib ] [postscript] (Subsumed by Intersection types for explicit substitutions) [vBLL05] S. van Bakel, S. Lengrand, and P. Lescanne. The language X: circuits, computations and classical logic. In 9th Italian Conference on Theoretical Computer Science (ICTCS'05), Siena, Italy, volume 3701 of Lecture Notes in Computer Science, pages 81--96, October 2005. [ bib | http ]

## Dissertations, Reports, Talks

 [GL18] S. Graham-Lengrand. The intuitionistic calculus that was discovered 6 times,, November 2018. Talk at the Deducteam seminar 2018/11/08. [ bib | .pdf ] [AGLK18] B. Accattoli, S. Graham-Lengrand, and D. Kesner. Tight typings and split bounds - long version. Technical report, arXiv.org, 2018 [ bib | http ] [BGLS16] M. P. Bonacina, S. Graham-Lengrand, and N. Shankar. A model-constructing framework for theory combination. Technical Report RR-99/2016, Università degli Studi di Verona - SRI International - CNRS, September 2016. Revised in Feb. 2017 [ bib | http ] Slides: [pdf] [GL15] S. Graham-Lengrand. Slot machines: an approach to the strategy challenge in SMT solving (presentation only), July 2015 [ bib | http ] [RFGL+14] D. Rouhling, M. Farooque, S. Graham-Lengrand, J.-M. Notin, and A. Mahboubi. Axiomatic constraint systems for proof search modulo theories. Technical report, Laboratoire d'informatique de l'École Polytechnique - CNRS, Microsoft Research - INRIA Joint Centre, Parsifal & TypiCal - INRIA Saclay, France, December 2014 [ bib | http ] [GGL16] D. Galmiche and S. Graham-Lengrand. Special issue on computational logic in honour of Roy Dyckhoff. volume 26(2) of Journal of Logic and Computation. Oxford University Press, 2016. Published online in 2014. [ bib | DOI ] [GL14a] S. Graham-Lengrand. Polarities & Focussing: a journey from Realisability to Automated Reasoning. Habilitation thesis, Université Paris-Sud, 2014. [ bib | http ] Publicly defended on 17th December 2014 before Wolfgang Ahrendt (rapporteur) Hugo Herbelin (rapporteur) Frank Pfenning (rapporteur) Sylvain Conchon David Delahaye Didier Galmiche Laurent Regnier Christine Paulin-Mohring [The webpage] [GL14b] S. Graham-Lengrand. Polarities & focussing: a journey from realisability to automated reasoning -- Coq proofs of Part II, 2014 [ bib | http ] [BGL13] A. Bernadet and S. Graham-Lengrand. A big-step operational semantics via non-idempotent intersection types, 2013. [ bib | .pdf ] [FGL13] M. Farooque and S. Graham-Lengrand. Sequent calculi with procedure calls. Technical report, Laboratoire d'informatique de l'École Polytechnique - CNRS, Parsifal - INRIA Saclay, France, January 2013 [ bib | http ] [BGL12] A. Bernadet and S. Graham-Lengrand. A simple presentation of the effective topos. Technical report, Laboratoire d'informatique de l'École Polytechnique - CNRS, France, April 2012 [ bib | http ] [FLM12a] M. Farooque, S. Lengrand, and A. Mahboubi. Simulating the DPLL(T) procedure in a sequent calculus with focusing. Technical report, Laboratoire d'informatique de l'École Polytechnique - CNRS, Microsoft Research - INRIA Joint Centre, Parsifal & TypiCal - INRIA Saclay, France, March 2012 [ bib | http ] [FLM12b] M. Farooque, S. Lengrand, and A. Mahboubi. Two simulations about DPLL(T). Technical report, Laboratoire d'informatique de l'École Polytechnique - CNRS, Microsoft Research - INRIA Joint Centre, Parsifal & TypiCal - INRIA Saclay, France, March 2012 [ bib | http ] [Len12] S. Lengrand. L'ordinateur peut-il allier raisonnement logique et techniques calculatoires ? In Intelligence Artificielle et Robotique, volume 4 of Les cahiers de l'ANR. ANR, 2012. [ bib | http ] [BL11] A. Bernadet and S. Lengrand. Filter models: non-idempotent intersection types, orthogonality and polymorphism - long version. Technical report, LIX, CNRS-INRIA-Ecole Polytechnique, June 2011 [ bib | http ] [Len08] S. Lengrand. Termination of lambda-calculus with the extra call-by-value rule known as assoc. Technical report, LIX, CNRS-INRIA-Ecole Polytechnique, January 2008 [ bib | http ] [Len06] S. Lengrand. Normalisation & Equivalence in Proof Theory & Type Theory. PhD thesis, Université Paris 7 & University of St Andrews, 2006. [ bib ] Supervised by Pr. Delia KESNER & Dr Roy DYCKHOFF. Publicly defended on 8th December 2006 before Dr Pierre-Louis CURIEN, Chairman Dr James McKINNA, Internal examiner of St Andrews Pr. Gilles DOWEK, Referee (rapporteur) for Paris VII Pr. Luke ONG, Referee (rapporteur) for St Andrews Pr. Henk BARENDREGT, Examiner Pr. Dale MILLER, Examiner & my supervisors. For this thesis I was one of the three recipients of the 2007 Ackermann Award, the EACSL Outstanding Dissertation Award for Logic in Computer Science, presented at the conference CSL'2007 in Lausanne. [The dissertation (pdf) 2522 Kb] [with a synopsis in French (pdf) 2609 Kb] Abstract (In French) [Len05] S. Lengrand. Induction principles as the foundation of the theory of normalisation: Concepts and techniques. Technical report, PPS laboratory, Université Paris 7, March 2005 [ bib | http ]