Home
Publications
Teaching
The Psyche prover
The Ψ project

Dr Stéphane GrahamLengrand Chargé de Recherche au CNRS




Current work
[RFGL^{+}14]

D. Rouhling, M. Farooque, S. GrahamLengrand, A. Mahboubi, and J.M.
Notin.
Axiomatisation of constraint systems to specify a tableaux calculus
modulo theories.
2014.
[ bib ]
[pdf]

Journal papers (published or accepted)
[GGL14]

D. Galmiche and S. GrahamLengrand.
Special issue on computational logic in honour of Roy Dyckhoff.
Journal of Logic and Computation, 2014.
[ bib 
DOI 
http ]

[BGL13]

A. Bernadet and S. GrahamLengrand.
Nonidempotent intersection types and strong normalisation.
Logical Methods in Computer Science, 9(4), 2013.
[ bib ]
[pdf] (Subsumes
Complexity of strongly
normalising $\lambda$terms via nonidempotent
intersection types and Filter
models: nonidempotent intersection types,
orthogonality and polymorphism)

[LDM11]

S. Lengrand, R. Dyckhoff, and J. McKinna.
A focused sequent calculus framework for proof search in Pure
Type Systems.
Logical Methods in Computer Science, 7(1), 2011.
[ bib ]
[pdf] (Subsumes
A sequent calculus for Type Theory)

[GL09]

M. Gabbay and S. Lengrand.
The λcontext calculus.
Information and Computation, 207(12):13691400, 2009.
[ bib ]
(Subsumes The lambdacontext
calculus)

[LM08]

S. Lengrand and A. Miquel.
Classical F_{ω}, orthogonality and symmetric candidates.
Annals of Pure and Applied Logic, 153:320, 2008.
[ bib ]
[pdf] (Subsumes
A classical version of Fomega)

[DL07]

R. Dyckhoff and S. Lengrand.
Callbyvalue λcalculus and LJQ.
Journal of Logic and Computation, 17:11091134, 2007.
[ bib ]
[pdf] The proof of strong
normalisation of LJQ:
[pdf] (updated in December
2007)

[KL07]

D. Kesner and S. Lengrand.
Resource operators for the λcalculus.
Information and Computation, 205:419473, 2007.
[ bib ]
[pdf] (Subsumes
Extending the Explicit
Substitution Paradigm)

[LLD^{+}04]

S. Lengrand, P. Lescanne, D. Dougherty, M. DezaniCiancaglini, and
S. van Bakel.
Intersection types for explicit substitutions.
Information and Computation, 189(1):1742, 2004.
[ bib ]
[pdf] (Subsumes
An improved system of
intersection types for explicit substitutions)

Reviewed Conference and Workshop papers (published or accepted)
[GL13]

S. GrahamLengrand.
Psyche: a proofsearch engine based on sequent calculus with an
LCFstyle architecture.
In D. Galmiche and D. LarcheyWendling, editors, Proceedings of
the 22nd International Conference on Automated Reasoning with Analytic
Tableaux and Related Methods (Tableaux'13), volume 8123 of Lecture
Notes in Computer Science, pages 149156. SpringerVerlag, September
2013.
[ bib ]
[pdf]

[FGLM13]

M. Farooque, S. GrahamLengrand, and A. Mahboubi.
A bisimulation between DPLL(T) and a proofsearch strategy for the
focused sequent calculus.
In A. Momigliano, B. Pientka, and R. Pollack, editors,
Proceedings of the 2013 International Workshop on Logical Frameworks
and MetaLanguages: Theory and Practice (LFMTP 2013). ACM Press, September
2013.
[ bib 
DOI ]
[pdf]

[BL11b]

A. Bernadet and S. Lengrand.
Filter models: nonidempotent intersection types, orthogonality and
polymorphism.
In M. Bezem, editor, Proceedings of the 20th Annual Conference
of the European Association for Computer Science Logic (CSL'11), Leibniz
International Proceedings in Informatics. Schloss Dagstuhl Leibniz Center for
Informatics, September 2011.
[ bib ]
[pdf]

[BL11a]

A. Bernadet and S. Lengrand.
Complexity of strongly normalising λterms via nonidempotent
intersection types.
In M. Hofmann, editor, Proceedings of the 14th International
Conference on Foundations of Software Science and Computation Structures
(FOSSACS'11), volume 6604 of Lecture Notes in Computer Science.
SpringerVerlag, March 2011.
[ bib ]
[pdf]

[KL08]

K. Kikuchi and S. Lengrand.
Strong normalisation of cutelimination that simulates
βreduction.
In R. Amadio, editor, Proceedings of the 11th International
Conference on Foundations of Software Science and Computation Structures
(FOSSACS'08), volume 4962 of Lecture Notes in Computer Science, pages
380394. SpringerVerlag, March 2008.
[ bib ]
[pdf] Long version:
[pdf]

[GL08]

M. Gabbay and S. Lengrand.
The lambdacontext calculus.
volume 196 of Electronic Notes in Theoretical Computer
Science, pages 1935, 2008.
Revision from the Second International Workshop on Logical Frameworks
and MetaLanguages: Theory and Practice (LFMTP 2007) (was A(nother) NEW
Calculus of Contexts).
[ bib ]
[pdf] (Subsumed by
The lambdacontext Calculus)

[LDM06]

S. Lengrand, R. Dyckhoff, and J. McKinna.
A sequent calculus for type theory.
In Z. Esik, editor, Proceedings of the 15th Annual Conference
of the European Association for Computer Science Logic (CSL'06), volume 4207
of Lecture Notes in Computer Science, pages 441455. SpringerVerlag,
September 2006.
[ bib ]
[pdf] (Subsumed by
A Focused Sequent Calculus Framework
for Proof Search in Pure Type Systems)

[DKL06]

R. Dyckhoff, D. Kesner, and S. Lengrand.
Strong cutelimination systems for Hudelmaier's depthbounded
sequent calculus for implicational logic.
In U. Furbach and N. Shankar, editors, Proceedings of the 3rd
International Joint Conference on Automated Reasoning (IJCAR'06), volume
4130 of Lecture Notes in Artificial Intelligence, pages 347361.
SpringerVerlag, August 2006.
[ bib ]
[pdf] Long version:
[pdf]

[DL06]

R. Dyckhoff and S. Lengrand.
LJQ, a strongly focused calculus for intuitionistic logic.
In A. Beckmann, U. Berger, B. Loewe, and J. V. Tucker, editors,
Proceedings of the 2nd Conference on Computability in Europe (CiE'06),
volume 3988 of Lecture Notes in Computer Science, pages 173185.
SpringerVerlag, July 2006.
[ bib ]
[pdf] The proof of strong
normalisation of LJQ:
[pdf] (updated in December
2007)

[LM06]

S. Lengrand and A. Miquel.
A classical version of F_{ω}.
In S. van Bakel and S. Berardi, editors, 1st Workshop on
Classical logic and Computation, July 2006.
[ bib ]
[pdf] (Subsumed by
Classical Fomega, orthogonality and
symmetric candidates)

[BL05]

K. Brünnler and S. Lengrand.
On two forms of bureaucracy in derivations.
In F. L. Paola Bruscoli and J. Stewart, editors, 1st Workshop
on Structures and Deductions (SD'05), Technical Report, Technische
Universität Dresden, pages 6980, July 2005.
ISSN 1430211X.
[ bib ]
[pdf] Slides
[postscript]

[KL05]

D. Kesner and S. Lengrand.
Extending the explicit substitution paradigm.
In J. Giesl, editor, Proceedings of the 16th International
Conference on Rewriting Techniques and Applications (RTA'05), volume 3467 of
Lecture Notes in Computer Science, pages 407422. SpringerVerlag,
April 2005.
[ bib ]
[postscript] (Best paper
award RTA 2005) (Subsumed by Resource
operators for the lambdacalculus)

[Len04]

S. Lengrand.
Deriving strong normalisation.
In D. Kesner, F. van Raamsdonk, and J. Wells, editors, 2nd
International Workshop on HigherOrder Rewriting (HOR'04), Technical Report
AIB200403, RWTH Aachen, pages 8488, June 2004.
[ bib ]
[postscript] (Subsumed by
Induction principles as the
foundation of the theory of normalisation: concepts and
techniques)

[Len03]

S. Lengrand.
Callbyvalue, callbyname, and strong normalization for the
classical sequent calculus.
volume 86(4) of Electronic Notes in Theoretical Computer
Science. Elsevier, 2003.
Revision from the 3rd International Workshop on Reduction Strategies
in Rewriting and Programming (WRS'03).
[ bib ]
[postscript] Slides:
[postscript]
Erratum: [postscript]

[DLL02]

D. J. Dougherty, S. Lengrand, and P. Lescanne.
An improved system of intersection types for explicit substitutions.
In R. A. BaezaYates, U. Montanari, and N. Santoro, editors,
Proceedings of the IFIP 17th World Computer Congress  TC1 Stream / 2nd
IFIP International Conference on Theoretical Computer Science (TCS'02),
volume 223 of IFIP Conference Proceedings, pages 511523. Kluwer,
August 2002.
[ bib ]
[postscript] (Subsumed
by Intersection types for explicit
substitutions)

Dissertations and Reports
[GL14a]

S. GrahamLengrand.
Polarities & Focussing: a journey from Realisability to
Automated Reasoning.
Habilitation thesis, Université ParisSud, 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 PaulinMohring
[The webpage]

[GL14b]

S. GrahamLengrand.
Polarities & focussing: a journey from realisability to automated
reasoning  Coq proofs of Part II.
2014
[ bib 
http ]

[FGL13]

M. Farooque and S. GrahamLengrand.
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. GrahamLengrand.
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 ]

[BL11]

A. Bernadet and S. Lengrand.
Filter models: nonidempotent intersection types, orthogonality and
polymorphism  long version.
Technical report, LIX, CNRSINRIAEcole Polytechnique, June 2011
[ bib 
http ]

[Len08]

S. Lengrand.
Termination of lambdacalculus with the extra callbyvalue rule
known as assoc.
Technical report, LIX, CNRSINRIAEcole 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 PierreLouis 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 ]


