@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} }
This file was generated by bibtex2html 1.99.