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 |
https |
.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
|
[BGLV23]
|
M. P. Bonacina, S. Graham-Lengrand, and C. Vauthier.
QSMA: A new algorithm for quantified satisfiability modulo theory
and assignment.
In B. Pientka and C. Tinelli, editors, Proceedings of the 29th
International Conference on Automated Deduction (CADE'23). Springer-Verlag,
July 2023.
[ bib |
.pdf ]
|
|
[BGLS22]
|
M. P. Bonacina, S. Graham-Lengrand, and N. Shankar.
CDSAT for nondisjoint theories with shared predicates: Arrays with
abstract length.
In D. Déharbe and A. Hyvärinen, editors, 20th International
Workshop on Satisfiability Modulo Theories (SMT 2022), volume 3185 of
CEUR Workshop Proceedings, pages 18--37. CEUR-WS.org, August
2022.
[ bib |
.pdf ]
[slides]
|
|
[ABC+21]
|
J. B. Almeida, M. Barbosa, M. L. Correia, K. Eldefrawy,
S. Graham-Lengrand, H. Pacheco, and V. Pereira.
Machine-checked ZKP for NP relations: Formally verified security
proofs and implementations of mpc-in-the-head.
In Y. Kim, J. Kim, G. Vigna, and E. Shi, editors, CCS '21:
2021 ACM SIGSAC Conference on Computer and Communications Security,
pages 2587--2600. ACM Press, November 2021.
[ bib |
DOI |
https ]
|
|
[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
|
[GL21]
|
S. Graham-Lengrand.
From MCSAT to CDSAT and beyond, September 2021.
Dagstuhl seminar on Integrated Deduction.
[ bib |
DOI |
.pdf ]
|
|
[GL18]
|
S. Graham-Lengrand.
The intuitionistic calculus that was discovered 6 times, November
2018.
Talk at the Deducteam seminar.
[ bib |
.pdf ]
|
|
[AGLK18]
|
B. Accattoli, S. Graham-Lengrand, and D. Kesner.
Tight typings and split bounds - long version.
Technical report, arXiv.org, 2018
[ bib |
https ]
|
|
[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]
Report:
[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 |
https ]
|
|
[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 ]
|
|
