Uniform Circuits, & Boolean Proof Nets. - Virgile Mogbil; Vincent Rahli (LFCS, 2007)

A Complete Realisability Semantics for Intersection Types and Arbitrary Expansion Variables. - Fairouz Kamareddine; Karim Nour; Vincent Rahli; J. B. Wells (ICTAC, 2008)

Simplified Reducibility Proofs of Church-Rosser for beta- and betaeta-reduction. - Fairouz Kamareddine; Vincent Rahli (LSFA, 2008)

ShadowDB: A Replicated Database on a Synthesized Consensus Core. - Nicolas Schiper; Vincent Rahli; Robbert van Renesse; Mark Bickford; Robert L. Constable (HotDep, 2012)

A diversified and correct-by-construction broadcast service. - Vincent Rahli; Nicolas Schiper; Robbert van Renesse; Mark Bickford; Robert L. Constable (ICNP, 2012)

On Realisability Semantics for Intersection Types with Expansion Variables. - Fairouz Kamareddine; Karim Nour; Vincent Rahli; J. B. Wells (Fundam. Informaticae, 2012)

Reducibility Proofs in the λ-Calculus. - Fairouz Kamareddine; Vincent Rahli; J. B. Wells (Fundam. Informaticae, 2012)

Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types. - Vincent Rahli; Mark Bickford; Abhishek Anand (ITP, 2013)

Developing Correctly Replicated Databases Using Formal Tools. - Nicolas Schiper; Vincent Rahli; Robbert van Renesse; Mark Bickford; Robert L. Constable (DSN, 2014)

Towards a Formally Verified Proof Assistant. - Abhishek Anand; Vincent Rahli (ITP, 2014)

A Generic Approach to Proofs about Substitution. - Abhishek Anand; Vincent Rahli (LFMTP, 2014)

Skalpel: A Type Error Slicer for Standard ML. - Vincent Rahli; Joe B. Wells; John Pirie; Fairouz Kamareddine (LSFA, 2014)

Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML. - Vincent Rahli; David Guaspari; Mark Bickford; Robert L. Constable (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2015)

A nominal exploration of intuitionism. - Vincent Rahli; Mark Bickford (CPP, 2016)

Exercising Nuprl's Open-Endedness. - Vincent Rahli (ICMS, 2016)

Avoiding Leakage and Synchronization Attacks through Enclave-Side Preemption Control. - Marcus Völp; Adam Lackorzynski; Jérémie Decouchant; Vincent Rahli; Francisco Rocha; Paulo Jorge Esteves Veríssimo (SysTEX@Middleware, 2016)

Formally verified differential dynamic logic. - Rose Bohrer; Vincent Rahli; Ivana Vukotic; Marcus Völp; André Platzer (CPP, 2017)

Bar induction: The good, the bad, and the ugly. - Vincent Rahli; Mark Bickford; Robert L. Constable (LICS, 2017)

Meeting the Challenges of Critical and Extreme Dependability and Security. - Paulo Jorge Esteves Veríssimo; Marcus Völp; Jeremie Decouchant; Vincent Rahli; Francisco Rocha (PRDC, 2017)

Skalpel: A constraint-based type error slicer for Standard ML. - Vincent Rahli; Joe B. Wells; John Pirie; Fairouz Kamareddine (J. Symb. Comput., 2017)

EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems. - Vincent Rahli; David Guaspari; Mark Bickford; Robert L. Constable (Sci. Comput. Program., 2017)

Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. - Vincent Rahli; Ivana Vukotic; Marcus Völp; Paulo Jorge Esteves Veríssimo (ESOP, 2018)

Computability Beyond Church-Turing via Choice Sequences. - Mark Bickford; Liron Cohen 001; Robert L. Constable; Vincent Rahli (LICS, 2018)

A Verified Theorem Prover Backend Supported by a Monotonic Library. - Vincent Rahli; Liron Cohen 001; Mark Bickford (LPAR, 2018)

Validating Brouwer's continuity principle for numbers using named exceptions. - Vincent Rahli; Mark Bickford (Math. Struct. Comput. Sci., 2018)

Bar Induction is Compatible with Constructive Type Theory. - Vincent Rahli; Mark Bickford; Liron Cohen 001; Robert L. Constable (J. ACM, 2019)

Asphalion: trustworthy shielding against Byzantine faults. - Ivana Vukotic; Vincent Rahli; Paulo Jorge Esteves Veríssimo (Proc. ACM Program. Lang., 2019)

PISTIS: From a Word-of-Mouth to a Gentleman's Agreement. - David Kozhaya; Jeremie Decouchant; Vincent Rahli; Paulo Jorge Esteves Veríssimo (CoRR, 2020)

Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle. - Mark Bickford; Liron Cohen 001; Robert L. Constable; Vincent Rahli (CSL, 2021)

Practical Byzantine Reliable Broadcast on Partially Connected Networks. - Silvia Bonomi; Jérémie Decouchant; Giovanni Farina; Vincent Rahli; Sébastien Tixeuil (ICDCS, 2021)

PISTIS: An Event-Triggered Real-Time Byzantine-Resilient Protocol Suite. - David Kozhaya; Jérémie Decouchant; Vincent Rahli; Paulo Esteves Veríssimo (IEEE Trans. Parallel Distributed Syst., 2021)

DAMYSUS: streamlined BFT consensus leveraging trusted components. - Jérémie Decouchant; David Kozhaya; Vincent Rahli; Jiangshan Yu (EuroSys, 2022)

Constructing Unprejudiced Extensional Type Theories with Choices via Modalities. - Liron Cohen 001; Vincent Rahli (FSCD, 2022)

Realizing Continuity Using Stateful Computations. - Liron Cohen 001; Vincent Rahli (CSL, 2023)

Inductive Continuity via Brouwer Trees. - Liron Cohen 001; Bruno da Rocha Paiva; Vincent Rahli; Ayberk Tosun (MFCS, 2023)

Intrusion Resilience Systems for Modern Vehicles. - Ali Shoker; Vincent Rahli; Jérémie Decouchant; Paulo Esteves Veríssimo (VTC2023-Spring, 2023)

TT☐C: a Family of Extensional Type Theories with Effectful Realizers of Continuity. - Liron Cohen 001; Vincent Rahli (CoRR, 2023)

OneShot: View-Adapting Streamlined BFT Protocols with Trusted Execution Environments. - Jérémie Decouchant; David Kozhaya; Vincent Rahli; Jiangshan Yu (IPDPS, 2024)

Separating Markov's Principles. - Liron Cohen 001; Yannick Forster 002; Dominik Kirst; Bruno da Rocha Paiva; Vincent Rahli (LICS, 2024)

Reliable Communication in Hybrid Authentication and Trust Models. - Rowdy Chotkan; Bart Cox; Vincent Rahli; Jérémie Decouchant (OPODIS, 2024)

$ text{TT}^{ Box}_{ mathcal C}$: a Family of Extensional Type Theories with Effectful Realizers of Continuity. - Liron Cohen 001; Vincent Rahli (Log. Methods Comput. Sci., 2024)

Internal Effectful Forcing in System T. - Martín Hötzel Escardó; Bruno da Rocha Paiva; Vincent Rahli; Ayberk Tosun (FSCD, 2025)