@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bib2bib --remove html --expand -oc html/myproceedings.txt -ob html/myproceedings.bib -c '(author : "lengrand") & ($type = "INPROCEEDINGS") & !(note : "Submitted") & !(annotate : "hide")' abbrev.bib Main.bib crossrefs.bib}}
@inproceedings{pubsdoc:Bakeletal-ICTCS05,
booktitle = {9th Italian Conference on Theoretical Computer Science
(ICTCS'05), Siena, Italy},
title = {{The language X: circuits, computations and classical logic}},
volume = {3701},
series = {Lecture Notes in Computer Science},
author = {van Bakel, Steffen and Lengrand, Stéphane and Lescanne, Pierre},
pages = {81--96},
month = {October},
year = {2005},
url = {http://pubs.doc.ic.ac.uk/Bakeletal-ICTCS05/}
}
@inproceedings{lengdouglesc01,
author = {Daniel J. Dougherty and {St\'ephane} Lengrand and
Pierre Lescanne},
title = {An Improved System of Intersection Types for Explicit
Substitutions},
isbn = {1-4020-7181-7},
pages = {511--523},
crossref = {ifipTCS02}
}
@inproceedings{lengrand03call-by-value,
author = {{St\'ephane} Lengrand},
title = {Call-by-value, call-by-name, and strong normalization
for the classical sequent calculus},
series = {Electronic Notes in Theoretical Computer Science},
volume = {86},
number = 4,
publisher = {Elsevier},
note = {Revision from the 3rd International Workshop on
Reduction Strategies in Rewriting and Programming
(WRS'03)},
editor = {Bernhard Gramlich and Salvador Lucas},
year = {2003}
}
@inproceedings{lengrandHOR2004,
author = {{St\'ephane} Lengrand},
title = {Deriving Strong Normalisation},
crossref = {hor04},
pages = {84-88},
month = jun
}
@inproceedings{lengrandkesner,
author = {Delia Kesner and {St\'ephane} Lengrand},
title = {Extending the explicit substitution paradigm},
crossref = {rta05},
pages = {407-422},
annotate = {Best Paper Award}
}
@inproceedings{lengbruen05,
author = {Kai {Br\"unnler} and {St\'ephane} Lengrand},
title = {On Two Forms of Bureaucracy in Derivations},
booktitle = {1st Workshop on Structures and Deductions (SD'05)},
editor = {Paola Bruscoli, Francois Lamarche and James Stewart},
series = {Technical Report, Technische {Universit\"at} Dresden},
note = {ISSN 1430-211X},
month = jul,
year = 2005,
place = {Lisbon, Portugal},
pages = {69--80},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/SD05.pdf}
}
@inproceedings{LM06,
author = {{St\'ephane} Lengrand and Alexandre Miquel},
title = {A classical version of {$F_\omega$}},
booktitle = {1st Workshop on Classical logic and Computation},
editor = {Stephen van Bakel and Stefano Berardi},
month = jul,
year = 2006,
place = {Venice, Italy},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/CLaC2006.pdf}
}
@inproceedings{DyckhoffLengrand,
author = {Roy Dyckhoff and {St\'ephane} Lengrand},
title = {{\sf {LJQ}}, a strongly Focused Calculus for Intuitionistic
Logic},
booktitle = {Proceedings of the 2nd Conference on Computability in Europe (CiE'06)},
series = {Lecture Notes in Computer Science},
volume = {3988},
publisher = {Springer-Verlag},
editor = {A. Beckmann and U. Berger and B. Loewe and J. V. Tucker},
year = {2006},
month = jul,
pages = {173--185},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/cie.pdf}
}
@inproceedings{DKL06,
author = {Roy Dyckhoff and Delia Kesner and {St\'ephane} Lengrand},
title = {Strong cut-elimination systems for {Hudelmaier}'s depth-bounded
sequent calculus for implicational logic},
booktitle = {Proceedings of the 3rd International Joint Conference on Automated Reasoning
(IJCAR'06)},
series = {Lecture Notes in Artificial Intelligence},
volume = {4130},
publisher = {Springer-Verlag},
editor = {U. Furbach and N. Shankar},
year = {2006},
month = aug,
pages = {347--361},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/IJCAR2006.pdf}
}
@inproceedings{LDMcK06,
author = {{St\'ephane} Lengrand and Roy Dyckhoff and James McKinna},
title = {A sequent calculus for Type Theory},
crossref = {csl06},
pages = {441--455},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/CSL2006.pdf}
}
@inproceedings{GabbayLengrand08,
author = {Murdoch Gabbay and {St\'ephane} Lengrand},
title = {The lambda-context Calculus},
editor = {Brigitte Pientka and Carsten {Sch\"urmann}},
series = {Electronic Notes in Theoretical Computer Science},
volume = {196},
year = 2008,
pages = {19--35},
note = {Revision from the Second International Workshop on Logical
Frameworks and Meta-Languages: Theory and Practice (LFMTP 2007)
(was {\em A(nother) NEW Calculus of Contexts})},
doi = {10.1016/j.entcs.2007.09.015},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/LFMTP2007.pdf}
}
@inproceedings{kikleng08,
author = {Kentaro Kikuchi and {St\'ephane} Lengrand},
title = {Strong Normalisation of Cut-Elimination that Simulates
{\(\beta\)}-Reduction},
crossref = {fossacs08},
pages = {380--394},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/FOSSACS08.pdf}
}
@inproceedings{bernadetleng11,
author = {Alexis Bernadet and {St\'ephane} Lengrand},
title = {Complexity of strongly normalising $\lambda$-terms via
non-idempotent intersection types},
crossref = {fossacs11},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/FOSSACS11.pdf}
}
@inproceedings{bernadetleng11b,
author = {Alexis Bernadet and {St\'ephane} Lengrand},
title = {Filter models: non-idempotent intersection types,
orthogonality and polymorphism},
crossref = {csl11},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/CSL11.pdf}
}
@inproceedings{farooque13,
author = {Mahfuza Farooque and {St\'ephane} Graham-Lengrand and
Assia Mahboubi},
title = {A bisimulation between {DPLL(T)} and a proof-search
strategy for the focused sequent calculus},
year = 2013,
publisher = {ACM Press},
booktitle = {Proceedings of the 2013 International Workshop on Logical
Frameworks and Meta-Languages: Theory and Practice
(LFMTP 2013)},
editor = {Alberto Momigliano and Brigitte Pientka and Randy
Pollack},
month = sep,
place = {Boston, USA},
doi = {10.1145/2503887.2503892},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/DPLL-LK.pdf}
}
@inproceedings{GLPsyche13,
title = {{Psyche}: a proof-search engine based on sequent calculus with an
{LCF}-style architecture},
author = {{St\'ephane} Graham-Lengrand},
year = 2013,
pages = {149--156},
crossref = {tableaux13},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/Psyche.pdf}
}
@inproceedings{Rouhling15,
title = {Axiomatic constraint systems for proof search modulo
theories},
author = {Damien Rouhling and Mahfuza Farooque and St\'ephane
Graham-Lengrand and Assia Mahboubi and Jean-Marc Notin},
crossref = {frocos15},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/FroCoS2015.pdf}
}
@inproceedings{GrahamLengrandWoF15,
author = {Graham-Lengrand, St\'ephane},
year = {2015},
title = {Realisability semantics of abstract focussing,
formalised},
editor = {Cervesato, Iliano and {Sch\"urmann}, Carsten},
booktitle = {Proceedings of the the First International Workshop on Focusing},
place = {Suva, Fiji},
month = nov,
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {197},
publisher = {Open Publishing Association},
pages = {15-28},
doi = {10.4204/EPTCS.197.3}
}
@inproceedings{BonacinaGrahamLengrandShankar:17,
title = {Satisfiability Modulo Theories and Assignments},
author = {Maria Paola Bonacina and Stéphane Graham-Lengrand and Natarajan
Shankar},
crossref = {cade17},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/CDSATpaper.pdf}
}
@inproceedings{GrahamLengrandSMT17,
author = {{St\'ephane} Graham-Lengrand and Dejan Jovanovi{\'c}},
title = {An {MCSAT} treatment of Bit-Vectors},
booktitle = {15th International Workshop on Satisfiability Modulo Theories
(SMT 2017)},
editor = {Martin Brain and Liana Hadarean},
year = {2017},
month = jul,
place = {Heidelberg, Germany},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/SMT2017.pdf}
}
@inproceedings{BonacinaGrahamLengrandShankar:18,
title = {Proofs in Conflict-Driven Theory Combination},
author = {Maria Paola Bonacina and Stéphane Graham-Lengrand and Natarajan
Shankar},
pages = {186--200},
url = {http://doi.acm.org/10.1145/3167096},
doi = {10.1145/3167096},
crossref = {cpp18},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/CDSATproofs.pdf}
}
@inproceedings{GrahamLengrandFarber:18,
title = {Guiding {SMT} Solvers with {Monte Carlo Tree Search} and Neural
Networks},
author = {Stéphane Graham-Lengrand and Michael Färber},
booktitle = {Third Conference on Artificial Intelligence and Theorem Proving
(AITP'2018)},
editor = {Thomas C. Hales and Cezary Kaliszyk and Stephan Schulz and Josef
Urban},
year = {2018},
month = mar,
place = {Aussois, France}
}
@inproceedings{AccattoliGrahamLengrandKesner:18,
title = {Tight Typings and Split Bounds},
author = {Beniamino Accattoli and Stéphane Graham-Lengrand and Delia
Kesner},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/2018-TightTypings.pdf},
crossref = {icfp18}
}
@inproceedings{BobotGLBM:SMT18,
author = {{Fran\,cois} Bobot and {St\'ephane} Graham-Lengrand and Bruno
Marre and Guillaume Bury},
title = {Centralizing Equality Reasoning in {MCSAT}},
booktitle = {16th International Workshop on Satisfiability Modulo Theories
(SMT 2018)},
editor = {Rayna Dimitrova and Vijay D'Silva },
year = {2018},
month = jul,
place = {Oxford, UK}
}
@inproceedings{GrahamLengrandSMT19,
author = {{St\'ephane} Graham-Lengrand and Dejan Jovanovi{\'c}},
title = {Interpolating bit-vector arithmetic constraints in {MCSAT}},
booktitle = {17th International Workshop on Satisfiability Modulo Theories
(SMT 2019)},
editor = {Natasha Sharygina and Joe Hendrix},
year = {2019},
month = jul,
place = {Lisbon, Portugal},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/SMT2019.pdf}
}
@inproceedings{FGGL:Tableaux19,
author = {Camillo Fiorentini and Rajeev Gor\'e and St\'ephane
Graham-Lengrand},
title = {A proof-theoretic perspective on {SMT}-solving for intuitionistic
propositional logic},
crossref = {tableaux19},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/2019-07-G4-SMT-Tableaux19.pdf}
}
@inproceedings{GrahamLengrandJovanovicDutertre:IJCAR2020,
author = {{St\'ephane} Graham-Lengrand and Dejan Jovanovi{\'c} and Bruno Dutertre},
title = {Solving bitvectors with {MCSAT}: explanations from bits and pieces},
crossref = {ijcar20},
month = jan,
number = {1},
pages = {103--121},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/IJCAR2020.pdf}
}
@inproceedings{AlmeidaBCEG0P21,
author = {Jos{\'{e}} Bacelar Almeida and
Manuel Barbosa and
Manuel L. Correia and
Karim Eldefrawy and
St{\'{e}}phane Graham{-}Lengrand and
Hugo Pacheco and
Vitor Pereira},
title = {Machine-checked {ZKP} for {NP} relations: Formally Verified Security
Proofs and Implementations of MPC-in-the-Head},
pages = {2587--2600},
crossref = {ccs2021},
url = {https://doi.org/10.1145/3460120.3484771},
doi = {10.1145/3460120.3484771}
}
@inproceedings{BonacinaSMT22,
title = {{CDSAT} for Nondisjoint Theories with Shared Predicates: Arrays With Abstract Length},
author = {Maria Paola Bonacina and Stéphane Graham-Lengrand and Natarajan
Shankar},
booktitle = {20th International Workshop on Satisfiability Modulo Theories
(SMT 2022)},
editor = {David D\'eharbe and Antti Hyv\"arinen},
series = {{CEUR} Workshop Proceedings},
volume = {3185},
pages = {18-37},
publisher = {CEUR-WS.org},
year = {2022},
month = aug,
place = {Haifa, Israel},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/SMT2022.pdf}
}
@inproceedings{BonacinaCADE23,
author = {Maria Paola Bonacina and Stéphane Graham-Lengrand and Christophe Vauthier},
title = {{QSMA}: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment},
crossref = {cade23},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/CADE2023.pdf}
}
@inproceedings{DBLP:conf/ccs/DittmerEG0O023,
author = {Samuel Dittmer and
Karim Eldefrawy and
St{\'{e}}phane Graham{-}Lengrand and
Steve Lu and
Rafail Ostrovsky and
Vitor Pereira},
title = {Boosting the Performance of High-Assurance Cryptography: Parallel
Execution and Optimizing Memory Access in Formally-Verified Line-Point
Zero-Knowledge},
pages = {2098--2112},
crossref = {ccs2023},
url = {https://doi.org/10.1145/3576915.3616583},
doi = {10.1145/3576915.3616583}
}
@inproceedings{DBLP:conf/smt/IrfanG24,
author = {Ahmed Irfan and
St{\'{e}}phane Graham{-}Lengrand},
editor = {Giles Reger and
Yoni Zohar},
title = {Arrays Reasoning in {MCSat}},
booktitle = {22nd International Workshop on Satisfiability Modulo Theories
(SMT 2024)},
series = {{CEUR} Workshop Proceedings},
volume = {3725},
pages = {24--35},
publisher = {CEUR-WS.org},
year = {2024},
month = jul,
place = {Montreal, Canada},
url = {https://ceur-ws.org/Vol-3725/paper11.pdf}
}
@inproceedings{DBLP:conf/ijcar/HaderKIGK24,
author = {Thomas Hader and
Daniela Kaufmann and
Ahmed Irfan and
St{\'{e}}phane Graham{-}Lengrand and
Laura Kov{\'{a}}cs},
title = {{MCSat}-Based Finite Field Reasoning in the Yices2 {SMT} Solver (Short
Paper)},
crossref = {ijcar24},
url = {https://doi.org/10.1007/978-3-031-63498-7\_23},
doi = {10.1007/978-3-031-63498-7\_23}
}
@inproceedings{LippariniCADE25,
author = {Enrico Lipparini and Thomas Hader and Ahmed Irfan and Stéphane Graham-Lengrand},
title = {Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search},
crossref = {cade25},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/2025-CADE.pdf}
}
@inproceedings{HaderCAV25,
author = {Thomas Hader and Ahmed Irfan and Stéphane Graham-Lengrand},
title = {Decision Heuristics in MCSat},
crossref = {cav25},
pdf = {http://www.csl.sri.com/users/sgl/Work/Reports/2025-CAV.pdf}
}
@proceedings{cade17,
booktitle = {Proceedings of the 26th International Conference on Automated Deduction
(CADE'17)},
publisher = {Springer-Verlag},
editor = {Leonardo de Moura},
series = {Lecture Notes in Artificial Intelligence},
volume = {10395},
year = {2017},
month = aug,
place = {Gothenburg, Sweden}
}
@proceedings{cade23,
booktitle = {Proceedings of the 29th International Conference on Automated Deduction
(CADE'23)},
publisher = {Springer-Verlag},
editor = {Brigitte Pientka and Cesare Tinelli},
year = {2023},
month = jul,
place = {Rome, Italy}
}
@proceedings{cade25,
booktitle = {Proceedings of the 30th International Conference on Automated Deduction
(CADE'25)},
publisher = {Springer-Verlag},
editor = {Clark Barrett and Uwe Waldmann},
year = {2025},
month = jul,
place = {Stuttgart, Germany}
}
@proceedings{cav25,
editor = {Ruzica Piskac and Zvonimir Rakamaric},
booktitle = {Proceedings of the 37th International Conference on Computer Aided
Verification (CAV'25)},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
year = {2025},
month = jul,
place = {Zagreb, Croatia}
}
@proceedings{ccs2021,
editor = {Yongdae Kim and
Jong Kim and
Giovanni Vigna and
Elaine Shi},
booktitle = {{CCS} '21: 2021 {ACM} {SIGSAC} Conference on Computer and Communications
Security},
publisher = {ACM Press},
place = {Virtual Event, Republic of Korea},
month = nov,
year = {2021},
url = {https://doi.org/10.1145/3460120},
doi = {10.1145/3460120},
isbn = {978-1-4503-8454-4}
}
@proceedings{ccs2023,
editor = {Weizhi Meng and
Christian Damsgaard Jensen and
Cas Cremers and
Engin Kirda},
booktitle = {{CCS} '23: 2023 {ACM} {SIGSAC} Conference on Computer and Communications
Security},
publisher = {ACM Press},
place = {Copenhagen, Denmark},
month = nov,
year = {2023},
url = {https://doi.org/10.1145/3576915},
doi = {10.1145/3576915}
}
@proceedings{cpp18,
editor = {June Andronick and Amy Felty},
booktitle = {Proceedings of the 7th International Conference on Certified Programs and
Proofs (CPP'18)},
publisher = {ACM Press},
year = {2018},
month = jan,
place = {Los Angeles, USA}
}
@proceedings{csl06,
booktitle = {Proceedings of the 15th Annual Conference of the European
Association for Computer Science Logic (CSL'06)},
editor = {Zoltan Esik},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = 4207,
month = sep,
year = 2006,
place = {Szeged, Hungary}
}
@proceedings{csl11,
booktitle = {Proceedings of the 20th Annual Conference of the European
Association for Computer Science Logic (CSL'11)},
editor = {Marc Bezem},
month = sep,
date = {12-15 September 2011},
year = 2011,
place = {Bergen, Norway},
publisher = {Schloss Dagstuhl Leibniz Center for Informatics},
series = {Leibniz International Proceedings in Informatics}
}
@proceedings{fossacs08,
booktitle = {Proceedings of the 11th International Conference on Foundations of
Software Science and Computation Structures (FOSSACS'08)},
editor = {Roberto Amadio},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = 4962,
month = mar,
year = 2008,
place = {Budapest, Hungary}
}
@proceedings{fossacs11,
booktitle = {Proceedings of the 14th International Conference on Foundations of
Software Science and Computation Structures (FOSSACS'11)},
editor = {Martin Hofmann},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {6604},
month = mar,
year = 2011,
place = {Saarbruecken, Germany}
}
@proceedings{frocos15,
editor = {Carsten Lutz and Silvio Ranise},
booktitle = {Proceedings of the 9th International Symposium on Frontiers of Combining Systems
(FroCoS'15)},
series = {Lecture Notes in Artificial Intelligence},
volume = {9322},
publisher = {Springer-Verlag},
year = 2015,
month = sep,
place = {Wroclaw, Poland}
}
@proceedings{hor04,
editor = {Delia Kesner and Femke {van Raamsdonk} and Joe Wells},
booktitle = {2nd International Workshop on Higher-Order Rewriting (HOR'04)},
series = {Technical Report AIB-2004-03, RWTH Aachen},
month = jun,
year = {2004},
place = {Aachen, Germany},
url = {\texttt{http://aib.informatik.rwth-aachen.de/2004/2004-03.ps.gz}}
}
@proceedings{icfp18,
booktitle = {Proceedings of the 23rd ACM International Conference on Functional Programming},
publisher = {ACM Press},
year = 2018,
editor = {Matthew Flatt}
}
@proceedings{ifipTCS02,
editor = {Ricardo A. Baeza-Yates and Ugo Montanari and Nicola
Santoro},
booktitle = {Proceedings of the IFIP 17th World Computer Congress - TC1 Stream /
2nd IFIP International Conference on Theoretical
Computer Science (TCS'02)},
publisher = {Kluwer},
series = {IFIP Conference Proceedings},
volume = {223},
year = {2002},
month = aug,
place = {{Montr\'eal}, Canada},
isbn = {1-4020-7181-7}
}
@proceedings{ijcar20,
editor = {Nicolas Peltier and Viorica Sofronie-Stokkermans},
booktitle = {Proceedings of the 10th International Joint Conference on
Automated Reasoning (IJCAR'20)},
place = {Paris, France},
year = {2020},
month = jul,
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {12166}
}
@proceedings{ijcar24,
editor = {Christoph Benzm{\"{u}}ller and
Marijn J. H. Heule and
Renate A. Schmidt},
booktitle = {Proceedings of the 12th International Joint Conference on
Automated Reasoning (IJCAR'24)},
place = {Nancy, France},
year = {2024},
month = jul,
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {14739}
}
@proceedings{rta05,
booktitle = {Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA'05)},
editor = {J\"urgen Giesl},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = 3467,
month = apr,
year = 2005,
place = {Nara, Japan}
}
@proceedings{tableaux13,
editor = {Didier Galmiche and Dominique Larchey-Wendling},
booktitle = {Proceedings of the 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux'13)},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = 8123,
year = {2013},
month = sep,
place = {Nancy, France}
}
@proceedings{tableaux19,
editor = {Andrei Popescu and Serenella Cerrito},
booktitle = {Proceedings of the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods
(Tableaux'19)},
publisher = {Springer-Verlag},
series = {Lecture Notes in Artificial Intelligence},
volume = 11714,
year = {2019},
month = sep,
place = {London, UK},
acronym = {Tableaux}
}
This file was generated by bibtex2html 1.99.