mymisc.bib

@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.