[BGLS18] |
M. P. Bonacina, S. Graham-Lengrand, and N. Shankar.
Proofs in conflict-driven theory combination.
In J. Andronick and A. Felty, editors, Proceedings of the 7th
International Conference on Certified Programs and Proofs (CPP'18). ACM
Press, January 2018.
[ bib ]
[pdf] |
[GLJ17] |
S. Graham-Lengrand and D. Jovanović.
An MCSAT treatment of bit-vectors.
In M. Brain and L. Hadarean, editors, 15 International Workshop
on Satisfiability Modulo Theories (SMT 2017), July 2017.
[ bib ]
[pdf] |
[BGLS17] |
M. P. Bonacina, S. Graham-Lengrand, and N. Shankar.
Satisfiability modulo theories and assignments.
In L. de Moura, editor, Proceedings of the 26th International
Conference on Automated Deduction (CADE'17), volume 10395 of Lecture
Notes in Artificial Intelligence. Springer-Verlag, August 2017.
[ bib ]
[pdf] Slides (08/2017): [pdf] |
[GL15] | S. Graham-Lengrand. Realisability semantics of abstract focussing, formalised. In I. Cervesato and C. Schürmann, editors, Proceedings of the the First International Workshop on Focusing, volume 197 of Electronic Proceedings in Theoretical Computer Science, pages 15--28. Open Publishing Association, November 2015. [ bib | DOI ] |
[RFGL^{+}15] |
D. Rouhling, M. Farooque, S. Graham-Lengrand, A. Mahboubi, and J.-M.
Notin.
Axiomatic constraint systems for proof search modulo theories.
In C. Lutz and S. Ranise, editors, Proceedings of the 9th
International Symposium on Frontiers of Combining Systems (FroCoS'15),
volume 9322 of Lecture Notes in Artificial Intelligence.
Springer-Verlag, September 2015.
[ bib ]
[pdf] |
[GL13] |
S. Graham-Lengrand.
Psyche: a proof-search engine based on sequent calculus with an
LCF-style architecture.
In D. Galmiche and D. Larchey-Wendling, 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 149--156. Springer-Verlag, September
2013.
[ bib ]
[pdf] |
[FGLM13] |
M. Farooque, S. Graham-Lengrand, and A. Mahboubi.
A bisimulation between DPLL(T) and a proof-search 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 Meta-Languages: Theory and Practice (LFMTP 2013). ACM Press, September
2013.
[ bib |
DOI ]
[pdf] |
[BL11b] |
A. Bernadet and S. Lengrand.
Filter models: non-idempotent 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 non-idempotent
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.
Springer-Verlag, March 2011.
[ bib ]
[pdf] |
[KL08] |
K. Kikuchi and S. Lengrand.
Strong normalisation of cut-elimination 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
380--394. Springer-Verlag, March 2008.
[ bib ]
[pdf] Long version: [pdf] |
[GL08] |
M. Gabbay and S. Lengrand.
The lambda-context calculus.
volume 196 of Electronic Notes in Theoretical Computer
Science, pages 19--35, 2008.
Revision from the Second International Workshop on Logical Frameworks
and Meta-Languages: Theory and Practice (LFMTP 2007) (was A(nother) NEW
Calculus of Contexts).
[ bib |
DOI ]
[pdf] (Subsumed by The lambda-context 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 441--455. Springer-Verlag,
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 cut-elimination systems for Hudelmaier's depth-bounded
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 347--361.
Springer-Verlag, 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 173--185.
Springer-Verlag, 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 69--80, July 2005.
ISSN 1430-211X.
[ 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 407--422. Springer-Verlag,
April 2005.
[ bib ]
[postscript] (Best paper award RTA 2005) (Subsumed by Resource operators for the lambda-calculus) |
[Len04] |
S. Lengrand.
Deriving strong normalisation.
In D. Kesner, F. van Raamsdonk, and J. Wells, editors, 2nd
International Workshop on Higher-Order Rewriting (HOR'04), Technical Report
AIB-2004-03, RWTH Aachen, pages 84--88, June 2004.
[ bib ]
[postscript] (Subsumed by Induction principles as the foundation of the theory of normalisation: concepts and techniques) |
[Len03] |
S. Lengrand.
Call-by-value, call-by-name, 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] |
[DLL02] |
D. J. Dougherty, S. Lengrand, and P. Lescanne.
An improved system of intersection types for explicit substitutions.
In R. A. Baeza-Yates, 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 511--523. Kluwer,
August 2002.
[ bib ]
[postscript] (Subsumed by Intersection types for explicit substitutions) |
This file was generated by bibtex2html 1.98.