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