[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 ]
[pdf] 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 ]
[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 ]
[BGL13] A. Bernadet and S. Graham-Lengrand. A big-step operational semantics via non-idempotent intersection types, 2013 [ bib | .pdf ]

This file was generated by bibtex2html 1.98.