Vincent Rahli

Publication Activity (10 Years)

Years Active: 2007-2024
Publications (10 Years): 29

Top Topics

Fair Exchange Protocols

Replicated Databases

Top Venues

Publications

Jérémie Decouchant, David Kozhaya, Vincent Rahli, Jiangshan Yu
OneShot: View-Adapting Streamlined BFT Protocols with Trusted Execution Environments. IPDPS (2024)
Liron Cohen, Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva, Vincent Rahli
Separating Markov's Principles. LICS (2024)
Liron Cohen, Vincent Rahli
$\text{TT}^{\Box}_{\mathcal C}$: a Family of Extensional Type Theories with Effectful Realizers of Continuity. Log. Methods Comput. Sci. 20 (2) (2024)
Ali Shoker, Vincent Rahli, Jeremie Decouchant, Paulo Esteves Veríssimo
Intrusion Resilience Systems for Modern Vehicles. CoRR (2023)
Liron Cohen, Vincent Rahli
: a Family of Extensional Type Theories with Effectful Realizers of Continuity. CoRR (2023)
Ali Shoker, Vincent Rahli, Jérémie Decouchant, Paulo Esteves Veríssimo
Intrusion Resilience Systems for Modern Vehicles. VTC2023-Spring (2023)
Liron Cohen, Bruno da Rocha Paiva, Vincent Rahli, Ayberk Tosun
Inductive Continuity via Brouwer Trees. MFCS (2023)
Liron Cohen, Vincent Rahli
Realizing Continuity Using Stateful Computations. CSL (2023)
Jérémie Decouchant, David Kozhaya, Vincent Rahli, Jiangshan Yu
DAMYSUS: streamlined BFT consensus leveraging trusted components. EuroSys (2022)
Liron Cohen, Vincent Rahli
Constructing Unprejudiced Extensional Type Theories with Choices via Modalities. FSCD (2022)
Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli
Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle. CSL (2021)
Silvia Bonomi, Jérémie Decouchant, Giovanni Farina, Vincent Rahli, Sébastien Tixeuil
Practical Byzantine Reliable Broadcast on Partially Connected Networks. ICDCS (2021)
David Kozhaya, Jérémie Decouchant, Vincent Rahli, Paulo Esteves Veríssimo
PISTIS: An Event-Triggered Real-Time Byzantine-Resilient Protocol Suite. IEEE Trans. Parallel Distributed Syst. 32 (9) (2021)
Silvia Bonomi, Jérémie Decouchant, Giovanni Farina, Vincent Rahli, Sébastien Tixeuil
Practical Byzantine Reliable Broadcast on Partially Connected Networks. CoRR (2021)
David Kozhaya, Jeremie Decouchant, Vincent Rahli, Paulo Jorge Esteves Veríssimo
PISTIS: From a Word-of-Mouth to a Gentleman's Agreement. CoRR (2020)
Ivana Vukotic, Vincent Rahli, Paulo Jorge Esteves Veríssimo
Asphalion: trustworthy shielding against Byzantine faults. Proc. ACM Program. Lang. 3 (OOPSLA) (2019)
Vincent Rahli, Mark Bickford, Liron Cohen, Robert L. Constable
Bar Induction is Compatible with Constructive Type Theory. J. ACM 66 (2) (2019)
Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli
Computability Beyond Church-Turing via Choice Sequences. LICS (2018)
Vincent Rahli, Ivana Vukotic, Marcus Völp, Paulo Jorge Esteves Veríssimo
Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. ESOP (2018)
Vincent Rahli, Mark Bickford
Validating Brouwer's continuity principle for numbers using named exceptions. Math. Struct. Comput. Sci. 28 (6) (2018)
Vincent Rahli, Liron Cohen, Mark Bickford
A Verified Theorem Prover Backend Supported by a Monotonic Library. LPAR (2018)
Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems. Sci. Comput. Program. 148 (2017)
Paulo Jorge Esteves Veríssimo, Marcus Völp, Jeremie Decouchant, Vincent Rahli, Francisco Rocha
Meeting the Challenges of Critical and Extreme Dependability and Security. PRDC (2017)
Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, André Platzer
Formally verified differential dynamic logic. CPP (2017)
Vincent Rahli, Mark Bickford, Robert L. Constable
Bar induction: The good, the bad, and the ugly. LICS (2017)
Vincent Rahli, Joe B. Wells, John Pirie, Fairouz Kamareddine
Skalpel: A constraint-based type error slicer for Standard ML. J. Symb. Comput. 80 (2017)
Vincent Rahli
Exercising Nuprl's Open-Endedness. ICMS (2016)
Vincent Rahli, Mark Bickford
A nominal exploration of intuitionism. CPP (2016)
Marcus Völp, Adam Lackorzynski, Jérémie Decouchant, Vincent Rahli, Francisco Rocha, Paulo Jorge Esteves Veríssimo
Avoiding Leakage and Synchronization Attacks through Enclave-Side Preemption Control. SysTEX@Middleware (2016)
Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 72 (2015)
Abhishek Anand, Vincent Rahli
A Generic Approach to Proofs about Substitution. LFMTP (2014)
Abhishek Anand, Vincent Rahli
Towards a Formally Verified Proof Assistant. ITP (2014)
Vincent Rahli, Joe B. Wells, John Pirie, Fairouz Kamareddine
Skalpel: A Type Error Slicer for Standard ML. LSFA (2014)
Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
Developing Correctly Replicated Databases Using Formal Tools. DSN (2014)
Vincent Rahli, Mark Bickford, Abhishek Anand
Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types. ITP (2013)
Fairouz Kamareddine, Karim Nour, Vincent Rahli, J. B. Wells
On Realisability Semantics for Intersection Types with Expansion Variables. Fundam. Informaticae 121 (1-4) (2012)
Vincent Rahli, Nicolas Schiper, Robbert van Renesse, Mark Bickford, Robert L. Constable
A diversified and correct-by-construction broadcast service. ICNP (2012)
Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
ShadowDB: A Replicated Database on a Synthesized Consensus Core. HotDep (2012)
Fairouz Kamareddine, Vincent Rahli, J. B. Wells
Reducibility Proofs in the λ-Calculus. Fundam. Informaticae 121 (1-4) (2012)
Fairouz Kamareddine, Karim Nour, Vincent Rahli, J. B. Wells
A Complete Realisability Semantics for Intersection Types and Arbitrary Expansion Variables. ICTAC (2008)
Fairouz Kamareddine, Vincent Rahli
Simplified Reducibility Proofs of Church-Rosser for beta- and betaeta-reduction. LSFA (2008)
Virgile Mogbil, Vincent Rahli
Uniform Circuits, & Boolean Proof Nets. LFCS (2007)