default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDStéphane Lengrand
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Books and Theses
- 2014
[b1]Stéphane Graham-Lengrand:
Polarities & Focussing: a journey from Realisability to Automated Reasoning. University of Paris-Sud, France, 2014
Journal Articles
- 2022
- [j12]Maria Paola Bonacina
, Stéphane Graham-Lengrand, Natarajan Shankar:
Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs. J. Autom. Reason. 66(1): 43-91 (2022) - 2020
- [j11]Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar:
Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness. J. Autom. Reason. 64(3): 579-609 (2020) - [j10]Beniamino Accattoli, Stéphane Graham-Lengrand, Delia Kesner:
Tight typings and split bounds, fully developed. J. Funct. Program. 30: e14 (2020) - 2018
- [j9]Beniamino Accattoli, Stéphane Graham-Lengrand, Delia Kesner:
Tight typings and split bounds. Proc. ACM Program. Lang. 2(ICFP): 94:1-94:30 (2018) - 2016
- [j8]Didier Galmiche, Stéphane Graham-Lengrand:
Special Issue on Computational Logic in Honour of Roy Dyckhoff. J. Log. Comput. 26(2): 463-465 (2016) - 2013
- [j7]Alexis Bernadet, Stéphane Lengrand:
Non-idempotent intersection types and strong normalisation. Log. Methods Comput. Sci. 9(4) (2013) - 2011
- [j6]Stéphane Lengrand, Roy Dyckhoff, James McKinna:
A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems. Log. Methods Comput. Sci. 7(1) (2011) - 2009
- [j5]Murdoch James Gabbay, Stéphane Lengrand:
The lambda-context calculus (extended version). Inf. Comput. 207(12): 1369-1400 (2009) - 2008
- [j4]Stéphane Lengrand, Alexandre Miquel:
Classical Fomega, orthogonality and symmetric candidates. Ann. Pure Appl. Log. 153(1-3): 3-20 (2008) - 2007
- [j3]Delia Kesner, Stéphane Lengrand:
Resource operators for lambda-calculus. Inf. Comput. 205(4): 419-473 (2007) - [j2]Roy Dyckhoff, Stéphane Lengrand:
Call-by-Value lambda-calculus and LJQ. J. Log. Comput. 17(6): 1109-1134 (2007) - 2004
- [j1]Stéphane Lengrand, Pierre Lescanne, Daniel J. Dougherty, Mariangiola Dezani-Ciancaglini, Steffen van Bakel:
Intersection types for explicit substitutions. Inf. Comput. 189(1): 17-42 (2004)
Conference and Workshop Papers
- 2024
- [c27]Thomas Hader, Daniela Kaufmann, Ahmed Irfan, Stéphane Graham-Lengrand, Laura Kovács:
MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver (Short Paper). IJCAR (1) 2024: 386-395 - [c26]Ahmed Irfan, Stéphane Graham-Lengrand:
Arrays Reasoning in MCSat. SMT@CAV 2024: 24-35 - 2023
- [c25]Maria Paola Bonacina, Stéphane Graham-Lengrand, Christophe Vauthier:
QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment. CADE 2023: 78-95 - [c24]Samuel Dittmer, Karim Eldefrawy, Stéphane Graham-Lengrand, Steve Lu, Rafail Ostrovsky, Vitor Pereira:
Boosting the Performance of High-Assurance Cryptography: Parallel Execution and Optimizing Memory Access in Formally-Verified Line-Point Zero-Knowledge. CCS 2023: 2098-2112 - 2022
- [c23]Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar:
CDSAT for Nondisjoint Theories with Shared Predicates: Arrays With Abstract Length. SMT 2022: 18-37 - 2021
- [c22]José Bacelar Almeida, Manuel Barbosa, Manuel L. Correia, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira:
Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head. CCS 2021: 2587-2600 - [c21]Salwa Tabet Gonzalez, Stéphane Graham-Lengrand, Julien Narboux, Natarajan Shankar:
Semantic parsing of geometry statements using supervised machine learning on synthetic data. CICM Workshops 2021 - 2020
- [c20]Stéphane Graham-Lengrand, Dejan Jovanovic, Bruno Dutertre:
Solving Bitvectors with MCSAT: Explanations from Bits and Pieces. IJCAR (1) 2020: 103-121 - 2019
- [c19]Camillo Fiorentini, Rajeev Goré, Stéphane Graham-Lengrand:
A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic. TABLEAUX 2019: 111-129 - 2018
- [c18]Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar:
Proofs in conflict-driven theory combination. CPP 2018: 186-200 - 2017
- [c17]Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar:
Satisfiability Modulo Theories and Assignments. CADE 2017: 42-59 - [c16]Stéphane Graham-Lengrand, Dejan Jovanovic:
An MCSAT treatment of Bit-Vectors. SMT 2017: 89-100 - 2015
- [c15]Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi, Jean-Marc Notin:
Axiomatic Constraint Systems for Proof Search Modulo Theories. FroCos 2015: 220-236 - [c14]Stéphane Graham-Lengrand:
Realisability semantics of abstract focussing, formalised. WoF'15 2015: 15-28 - 2013
- [c13]Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi:
A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus. LFMTP 2013: 3-14 - [c12]Stéphane Graham-Lengrand:
Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture. TABLEAUX 2013: 149-156 - 2011
- [c11]Alexis Bernadet, Stéphane Lengrand:
Filter Models: Non-idempotent Intersection Types, Orthogonality and Polymorphism. CSL 2011: 51-66 - [c10]Alexis Bernadet, Stéphane Lengrand:
Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types. FoSSaCS 2011: 88-107 - 2008
- [c9]Kentaro Kikuchi, Stéphane Lengrand:
Strong Normalisation of Cut-Elimination That Simulates beta-Reduction. FoSSaCS 2008: 380-394 - 2007
- [c8]Murdoch Gabbay, Stéphane Lengrand:
The lambda-context Calculus. LFMTP@CADE 2007: 19-35 - 2006
- [c7]Roy Dyckhoff, Delia Kesner, Stéphane Lengrand:
Strong Cut-Elimination Systems for Hudelmaier's Depth-Bounded Sequent Calculus for Implicational Logic. IJCAR 2006: 347-361 - [c6]Roy Dyckhoff, Stéphane Lengrand:
LJQ: A Strongly Focused Calculus for Intuitionistic Logic. CiE 2006: 173-185 - [c5]Stéphane Lengrand, Roy Dyckhoff, James McKinna:
A Sequent Calculus for Type Theory. CSL 2006: 441-455 - 2005
- [c4]Steffen van Bakel, Stéphane Lengrand, Pierre Lescanne:
The Language chi: Circuits, Computations and Classical Logic. ICTCS 2005: 81-96 - [c3]Delia Kesner, Stéphane Lengrand:
Extending the Explicit Substitution Paradigm. RTA 2005: 407-422 - 2003
- [c2]Stéphane Lengrand:
Call-by-value, call-by-name, and strong normalization for the classical sequent calculus. WRS 2003: 714-730 - 2002
- [c1]Daniel J. Dougherty, Stéphane Lengrand, Pierre Lescanne:
An Improved System of Intersection Types for Explicit Substitutions. IFIP TCS 2002: 511-523
Editorship
- 2023
- [e2]Stéphane Graham-Lengrand, Mathias Preiner:
Proceedings of the 21st International Workshop on Satisfiability Modulo Theories (SMT 2023) co-located with the 29th International Conference on Automated Deduction (CADE 2023), Rome, Italy, July, 5-6, 2023. CEUR Workshop Proceedings 3429, CEUR-WS.org 2023 [contents] - 2013
- [e1]Stéphane Graham-Lengrand, Luca Paolini:
Proceedings Sixth Workshop on Intersection Types and Related Systems, ITRS 2012, Dubrovnik, Croatia, 29th June 2012. EPTCS 121, 2013 [contents]
Informal and Other Publications
- 2024
- [i13]Thomas Hader, Daniela Kaufmann, Ahmed Irfan, Stéphane Graham-Lengrand, Laura Kovács:
MCSat-based Finite Field Reasoning in the Yices2 SMT Solver. CoRR abs/2402.17927 (2024) - 2023
- [i12]Samuel Dittmer, Karim Eldefrawy, Stéphane Graham-Lengrand, Steve Lu, Rafail Ostrovsky, Vitor Pereira:
Boosting the Performance of High-Assurance Cryptography: Parallel Execution and Optimizing Memory Access in Formally-Verified Line-Point Zero-Knowledge. IACR Cryptol. ePrint Arch. 2023: 1322 (2023) - 2021
- [i11]José Carlos Bacelar Almeida, Manuel Barbosa, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira:
Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head. CoRR abs/2104.05516 (2021) - [i10]José Bacelar Almeida, Manuel Barbosa, Manuel L. Correia, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira:
Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head. IACR Cryptol. ePrint Arch. 2021: 1149 (2021) - 2020
- [i9]Stéphane Graham-Lengrand, Dejan Jovanovic, Bruno Dutertre:
Solving bitvectors with MCSAT: explanations from bits and pieces (long version). CoRR abs/2004.07940 (2020) - 2018
- [i8]Beniamino Accattoli, Stéphane Graham-Lengrand, Delia Kesner:
Tight Typings and Split Bounds. CoRR abs/1807.02358 (2018) - 2014
- [i7]Stéphane Graham-Lengrand:
Polarities & Focussing: a journey from Realisability to Automated Reasoning. CoRR abs/1412.6781 (2014) - [i6]Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi, Jean-Marc Notin:
Axiomatisation of constraint systems to specify a tableaux calculus modulo theories. CoRR abs/1412.6790 (2014) - 2013
- [i5]Mahfuza Farooque, Stéphane Graham-Lengrand:
Sequent Calculi with procedure calls. CoRR abs/1304.6279 (2013) - [i4]Alexis Bernadet, Stéphane Graham-Lengrand:
A simple presentation of the effective topos. CoRR abs/1307.3832 (2013) - 2012
- [i3]Mahfuza Farooque, Stéphane Lengrand:
A sequent calculus with procedure calls. CoRR abs/1204.5156 (2012) - [i2]Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi:
Two simulations about DPLL(T). CoRR abs/1204.5159 (2012) - 2008
- [i1]Stéphane Lengrand:
Termination of lambda-calculus with the extra Call-By-Value rule known as assoc. CoRR abs/0806.4859 (2008)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-23 19:19 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
