54 citations · 67 across the 10 of their papers we have counts for
12 papers
Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head
José Carlos Bacelar Almeida, Manuel Barbosa, Karim Eldefrawy +3
MPC-in-the-Head (MitH) is a general framework that allows constructing efficient Zero Knowledge protocols for general NP-relations from secure multiparty computation (MPC) protocol…
Solving bitvectors with MCSAT: explanations from bits and pieces (long version)
Stéphane Graham-Lengrand, Dejan Jovanović, Bruno Dutertre
We present a decision procedure for the theory of fixed-sized bitvectors in the MCSAT framework. MCSAT is an alternative to CDCL(T) for SMT solving and can be seen as an extension…
Tight Typings and Split Bounds
Beniamino Accattoli, Stéphane Graham-Lengrand, Delia Kesner
Multi types---aka non-idempotent intersection types---have been used to obtain quantitative bounds on higher-order programs, as pioneered by de Carvalho. Notably, they bound at the…
Realisability semantics of abstract focussing, formalised
Stéphane Graham-Lengrand
We present a sequent calculus for abstract focussing, equipped with proof-terms: in the tradition of Zeilberger's work, logical connectives and their introduction rules are left as…
Polarities & Focussing: a journey from Realisability to Automated Reasoning
Stéphane Graham-Lengrand
This dissertation explores the roles of polarities and focussing in various aspects of Computational Logic. These concepts play a key role in the the interpretation of proofs as pr…
Non-idempotent intersection types and strong normalisation
Alexis Bernadet, Stéphane Jean Lengrand
We present a typing system with non-idempotent intersection types, typing a term syntax covering three different calculi: the pure λ-calculus, the calculus with explicit substituti…