@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bib2bib --remove html --expand -oc html/mymisc.txt -ob html/mymisc.bib -c '(author : "lengrand") & ($type <> "ARTICLE") & ($type <> "INPROCEEDINGS") & !(note : "Submitted") & !(annotate : "hide")' abbrev.bib Main.bib crossrefs.bib}}
@techreport{lengSNInd05,
author = {{St\'ephane} Lengrand},
title = {Induction principles as the foundation of the theory of
normalisation: Concepts and Techniques},
institution = {PPS laboratory, {Universit\'e} Paris 7},
year = 2005,
type = {Technical Report},
month = mar,
url = {http://hal.ccsd.cnrs.fr/ccsd-00004358}
}
@phdthesis{LengrandPhD,
author = {{St\'ephane} Lengrand},
title = {Normalisation \& Equivalence in Proof Theory \& Type
Theory},
school = {Universit{\'e} {Paris} 7 \& University of {St}
{Andrews}},
year = {2006}
}
@techreport{lengrand07tr,
author = {{St\'ephane} Lengrand},
title = {Termination of lambda-calculus with the extra
Call-By-Value rule known as assoc},
institution = {LIX, CNRS-INRIA-Ecole Polytechnique},
year = 2008,
month = jan,
url = {http://hal.inria.fr/inria-00292029}
}
@techreport{bernadetleng11blong,
author = {Alexis Bernadet and {St\'ephane} Lengrand},
title = {Filter models: non-idempotent intersection types,
orthogonality and polymorphism - Long version},
institution = {LIX, CNRS-INRIA-Ecole Polytechnique},
year = 2011,
month = jun,
url = {http://hal.archives-ouvertes.fr/hal-00600070/en/}
}
@incollection{Lengrand12ANR,
author = {St\'ephane Lengrand},
title = {L'ordinateur peut-il allier raisonnement logique et
techniques calculatoires~?},
booktitle = {{Intelligence Artificielle et Robotique}},
series = {Les cahiers de l'{ANR}},
volume = 4,
month = mar,
year = 2012,
publisher = {ANR},
address = {Paris},
url = {http://www.agence-nationale-recherche.fr/suivi-bilan/suivi-des-actions/consulter/intelligence-artificielle-et-robotique-confluences-de-l-homme-et-des-stic-cahier-anr-n4-mars-2012/}
}
@techreport{farooqueTR12,
url = {http://hal.archives-ouvertes.fr/hal-00690044},
title = {{Two simulations about DPLL(T)}},
author = {Farooque, Mahfuza and Lengrand, St{\'e}phane and
Mahboubi, Assia},
institution = {Laboratoire d'informatique de l'{\'E}cole
{Polytechnique} - {CNRS}, Microsoft Research - {INRIA
Joint Centre}, {Parsifal} \& {TypiCal} - {INRIA}
Saclay, France},
collaboration = {Project PSI: Proof-Search control in Interaction
with domain-specific methods },
year = {2012},
month = mar
}
@techreport{farooqueTR12b,
url = {http://hal.inria.fr/hal-00690392},
title = {{Simulating the DPLL(T) procedure in a sequent calculus
with focusing}},
author = {Farooque, Mahfuza and Lengrand, St{\'e}phane and
Mahboubi, Assia},
institution = {Laboratoire d'informatique de l'{\'E}cole
{Polytechnique} - {CNRS}, Microsoft Research - {INRIA
Joint Centre}, {Parsifal} \& {TypiCal} - {INRIA}
Saclay, France},
year = {2012},
month = mar
}
@techreport{bernadetlengrand12b,
author = {Alexis Bernadet and {St\'ephane} Graham-Lengrand},
title = {A simple presentation of the Effective Topos},
year = 2012,
month = apr,
institution = {Laboratoire d'informatique de l'{\'E}cole
{Polytechnique} - {CNRS}, France},
url = {http://hal.archives-ouvertes.fr/hal-00844250}
}
@techreport{farooqueTR13,
title = {Sequent calculi with procedure calls},
author = {Farooque, Mahfuza and Graham-Lengrand, St{\'e}phane},
year = {2013},
month = jan,
institution = {Laboratoire d'informatique de l'{\'E}cole
{Polytechnique} - {CNRS}, {Parsifal} - {INRIA} Saclay,
France},
url = {http://hal.archives-ouvertes.fr/hal-00779199},
annotate = {In this paper, we study 3 focussed sequent calculi that
are based on Miller-Liang's LKF system for polarised
classical logic, and integrate the possibility to call
a decision procedure. The main sequent calculus out of
the three is LK(T), in which we prove
cut-elimination. The second one is less focussed, and
is introduced for the proof that changing polarities do
not change provability, only the shape of proofs. The
third one features the possibility to polarise literals
"on the fly", and is used in other works to simulate
the DPLL(T) procedure. Finally, completeness of the 3
calculi is proved. Sequent calculus, polarities,
focusing, cut-elimination, completeness},
collaboration = {Project PSI: Proof-Search control in Interaction
with domain-specific methods }
}
@misc{bernadet13,
author = {Alexis Bernadet and Stéphane Graham-Lengrand},
title = {A big-step operational semantics via non-idempotent
intersection types},
year = 2013,
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/BigStep.pdf}
}
@misc{LengrandHDRCoq,
author = {{St\'ephane} Graham-Lengrand},
title = {Polarities \& Focussing: a journey from Realisability to Automated Reasoning -- {Coq} proofs of {Part II}},
school = {Universit{\'e} {Paris} 11},
year = {2014},
url = {http://www.lix.polytechnique.fr/\homedir lengrand/Work/HDR/}
}
@phdthesis{LengrandHDR,
author = {{St\'ephane} Graham-Lengrand},
title = {Polarities \& Focussing: a journey from Realisability
to Automated Reasoning},
school = {Universit{\'e} {Paris-Sud}},
type = {Habilitation thesis},
year = {2014},
url = {http://hal.archives-ouvertes.fr/tel-01094980}
}
@incollection{DyckhoffJLC,
author = {Galmiche, Didier and Graham-Lengrand, Stéphane},
editor = {Galmiche, Didier and Graham-Lengrand, Stéphane},
title = {Special Issue on Computational Logic in Honour of {Roy}
{Dyckhoff}},
year = {2016},
volume = {26},
number = {2},
note = {Published online in 2014},
doi = {10.1093/logcom/exu039},
series = {Journal of Logic and Computation},
publisher = {Oxford University Press}
}
@techreport{rouhling:hal-01107944,
title = {Axiomatic constraint systems for proof search modulo
theories},
author = {Rouhling, Damien and Farooque, Mahfuza and
Graham-Lengrand, St{\'e}phane and Notin, Jean-Marc and
Mahboubi, Assia},
url = {https://hal.inria.fr/hal-01107944},
institution = {Laboratoire d'informatique de l'{\'E}cole
{Polytechnique} - {CNRS}, Microsoft Research - {INRIA
Joint Centre}, {Parsifal} \& {TypiCal} - {INRIA}
Saclay, France},
collaboration = {Project PSI: Proof-Search control in Interaction
with domain-specific methods },
year = {2014},
month = dec,
hal_id = {hal-01107944}
}
@misc{GrahamLengrandSMT15,
author = {{St\'ephane} Graham-Lengrand},
title = {Slot Machines: an approach to the Strategy Challenge in
{SMT} solving (presentation only)},
booktitle = {13 International Workshop on Satisfiability Modulo
Theories (SMT'15)},
editor = {Vijay Ganesh and Dejan Jovanovi{\'c}},
year = {2015},
month = jul,
place = {San Francisco, USA},
url = {http://hal.archives-ouvertes.fr/hal-01211209}
}
@techreport{BonacinaGrahamLengrandShankar:16,
title = {A model-constructing framework for theory combination},
author = {Maria Paola Bonacina and Stéphane Graham-Lengrand and
Natarajan Shankar},
url = {http://hal.archives-ouvertes.fr/hal-01425305},
number = {RR-99/2016},
institution = {{Universit\`a degli Studi di Verona} - {SRI}
International - {CNRS}},
year = {2016},
month = sep,
note = {Revised in Feb. 2017}
}
@techreport{AccattoliGrahamLengrandKesner-long:18,
title = {Tight Typings and Split Bounds - long version},
author = {Beniamino Accattoli and Stéphane Graham-Lengrand and Delia
Kesner},
institution = {arXiv.org},
url = {https://arxiv.org/abs/1807.02358},
year = {2018}
}
@misc{GrahamLengrandG4SMT18,
author = {{St\'ephane} Graham-Lengrand},
title = {The intuitionistic calculus that was discovered 6 times},
note = {Talk at the Deducteam seminar},
year = {2018},
month = nov,
place = {Cachan, France},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/2018-11-08-Roy-G4-SMT.pdf}
}
@misc{GrahamLengrandDagstuhl2021,
author = {{St\'ephane} Graham-Lengrand},
title = {From {MCSAT} to {CDSAT} and beyond},
note = {Dagstuhl seminar on Integrated Deduction},
year = {2021},
doi = {10.4230/DagRep.11.8.35},
month = sep,
place = {Dagstuhl, Germany},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/2021-Dagstuhl-Graham-Lengrand.pdf}
}
@misc{lipparini2025boostingmcsatmodulononlinear,
title = {Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search},
author = {Enrico Lipparini and Thomas Hader and Ahmed Irfan and Stéphane Graham-Lengrand},
year = {2025},
eprint = {2503.01627},
archiveprefix = {arXiv},
primaryclass = {cs.LO},
url = {https://arxiv.org/abs/2503.01627}
}
This file was generated by bibtex2html 1.99.