Conference and Journal Papers

OneShot: ViewAdapting Streamlined BFT Protocols with Trusted Execution Environments
[pdf]
In collaboration with Jeremie Decouchant, David Kozhaya, and Jiangshan Yu
IPDPS 2024

Inductive Continuity via Brouwer Trees
[pdf]
[Github]
In collaboration with Liron Cohen, Bruno da Rocha Paiva, and Ayberk Tosun
MFCS 2023

Realizing Continuity Using Stateful Computations
[pdf]
[Github]
In collaboration with Liron Cohen
CSL 2023

Constructing Unprejudiced Extensional Type Theories with Choices via Modalities
[pdf]
[Github]
In collaboration with Liron Cohen
FSCD 2022

Damysus: Streamlined BFT Consensus Leveraging Trusted Components
[pdf]
[Github]
In collaboration with Jeremie Decouchant, David Kozhaya, and Jiangshan Yu
EuroSys 2022

Practical Byzantine Reliable Broadcast on Partially Connected Networks
[pdf]
In collaboration with Silvia Bonomi, Jeremie Decouchant, Giovanni Farina, and Sebastien Tixeuil
ICDCS 2021

PISTIS: An EventTriggered RealTime ByzantineResilient Protocol Suite
[pdf]
[Github]
In collaboration with David Kozhaya, Jeremie Decouchant, and Paulo Verissimo
IEEE Transactions on Parallel and Distributed Systems, 2021

Open Bar  a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle
[pdf]
[extended version]
[Github]
In collaboration with Liron Cohen, Mark Bickford and Robert L. Constable
CSL 2021

Asphalion: Trustworthy Shielding Against Byzantine Faults
[pdf]
[extended version]
[Github]
In collaboration with Ivana Vukotic and Paulo Verissimo
OOPSLA 2019

Bar Induction is Compatible with Constructive Type Theory
[pdf]
[Github]
Vincent Rahli Mark Bickford, Liron Cohen, and Robert L. Constable
JACM, 2019

A Verified Theorem Prover Backend Supported by a Monotonic Library
[pdf]
[Github]
Vincent Rahli, Liron Cohen, and Mark Bickford
LPAR 2018

Computability Beyond ChurchTuring via Choice Sequences
[pdf]
[extended version]
[Github]
In collaboration with Liron Cohen, Mark Bickford and Robert L. Constable
LICS 2018

Velisarios: Byzantine FaultTolerant Protocols Powered by Coq
[pdf]
[Github]
Vincent Rahli, Ivana Vukotic, Marcus Volp, and Paulo Verissimo
ESOP 2018

Validating Brouwer's Continuity Principle for Numbers Using Named Exceptions
[pdf]
[Github]
Vincent Rahli and Mark Bickford
MSCS, 2017

Bar Induction: The Good, the Bad, and the Ugly
[pdf]
[extended version]
[Github]
Vincent Rahli, Mark Bickford and Robert L. Constable
LICS 2017

Formally Verified Differential Dynamic Logic
[pdf]
[Github]
Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Volp and Andre Platzer
The 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017)

EventML: Specification, Verification, and Implementation of
CrashTolerant State Machine Replication Systems
[pdf]
[Github]
Vincent Rahli, David Guaspari, Mark Bickford, and Robert L. Constable
Science of Computer Programming journal, 2017

Exercising Nuprl's OpenEndedness
[pdf]
Vincent Rahli
The 5th International Congress on Mathematical Software (ICMS 2016)

A Nominal Exploration of Intuitionism
[pdf]
[Github]
Vincent Rahli and Mark Bickford
The 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016).

Skalpel: A ConstraintBased Type Error Slicer for Standard ML
[pdf]
[Github]
Vincent Rahli, J. B. Wells, John Pirie, and Fairouz Kamareddine
Special issue of the Journal of Symbolic Computation (JSC) on Program Verification, Automated Debugging and Symbolic Computation, 2016

Towards a Formally Verified Proof Assistant
[pdf]
[technical report]
[Github]
Abhishek Anand and Vincent Rahli
5th Conference on Interactive Theorem Proving (ITP 2014).

Developing Correctly Replicated Databases Using Formal Tools
[pdf]
[Github]
Nicolas Schiper, Vincent Rahli, Robbert Van Renesse, Mark Bickford, and Robert L. Constable
DSN 2014

Formal program optimization in Nuprl using
computational equivalence and partial types
[pdf]
[extended version]
Vincent Rahli, Mark Bickford, and Abhishek Anand
4th Conference on Interactive Theorem Proving (ITP 2013), Rennes, France, 2226 July 2013.

On Realisability Semantics for Intersection Types with Expansion Variables
[pdf]
Fairouz Kamareddine, Karim Nour, Vincent Rahli and J. B. Wells
Fundamenta Informaticae, volume 121, 2012

Reducibility proofs in the λcalculus
[pdf]
Fairouz Kamareddine, Vincent Rahli and J. B. Wells
Fundamenta Informaticae, volume 121, 2012 
A complete realisability semantics for intersection
types and arbitrary expansion variables
[pdf]
[slides]
[extended version]
Fairouz Kamareddine, Karim Nour, Vincent Rahli and J. B. Wells
5th International Colloquium on Theoretical Aspects of Computing (ICTAC 2008), The Marmara, Istanbul, Turkey, 13 September 2008.
Lecture Notes in Computer Science, volume 5160, Pages 171185.

Uniform circuits, & Boolean proof net
[pdf]
Virgile Mogbil and Vincent Rahli
Symposium on Logical Foundations of Computer Science (LFCS'07), New York, U.S.A., June 4  7 2007.
Lecture Notes in Computer Science, volume 4514, pages 401421.
Workshop Papers

Coq as a Metatheory for Nuprl with Bar Induction
[pdf]
[slides]
Vincent Rahli and Mark Bickford.
Presented at CCC 2015 .

Formal Specification, Verification, and Implementation
of FaultTolerant Systems Using EventML
[pdf]
[slides]
Vincent Rahli, David Guaspari, Mark Bickford, and Robert L. Constable
Presented at AVoCS 2015 .

Nuprl's Inductive Logical Forms
[pdf]
[slides]
Mark Bickford, Robert L. Constable, Rich Eaton, and Vincent Rahli
Presented at AI4FM 2015 .

A Type Theory With Partial Equivalence Relations as Types
[pdf]
[slides]
Abhishek Anand, Mark Bickford, Robert L. Constable, and Vincent Rahli
Accepted to TYPES 2014 .

A Diversified and CorrectbyConstruction Broadcast Service
[pdf]
[slides]
Vincent Rahli, Nicolas Schiper, Robbert Van Renesse, Mark Bickford, and Robert L. Constable
Accepted to WRiPE 2012, Austin, Texas, USA, October 30, 2012.

ShadowDB: A Replicated Database on a Synthesized
Consensus Core
[pdf]
Nicolas Schiper, Vincent Rahli, Robbert Van Renesse, Mark Bickford, and Robert L. Constable
Accepted to HotDep'12, Hollywood, CA, USA, October 7, 2012.

Interfacing with Proof Assistants for Domain Specific
Programming Using EventML
[pdf]
[slides]
Vincent Rahli
10th International Workshop on User Interfaces for Theorem Provers, Bremen, Germany, July 11th 2012.

The Logic of Events, a framework to reason about
distributed systems
[pdf]
[slides]
Mark Bickford, Vincent Rahli, and Robert L. Constable
Languages for Distributed Algorithms (LADA) workshop, Philadelphia, USA, 2324 January 2012.

Simplified Reducibility Proofs of ChurchRosser
for β and βηreduction
[pdf]
[slides]
[extended version]
Fairouz Kamareddine and Vincent Rahli
Third Workshop on Logical and Semantic Frameworks, with Applications (LSFA'08), Salvador, Bahia, Brasil, 26 August 2008.
Electronic Notes in Theoretical Computer Science, Volume 247, pages 85101

Reducibility proofs in the λcalculus
[pdf]
[slides]
[extended version]
Fairouz Kamareddine, Vincent Rahli and J. B. Wells,
ITRS'08, Torino, Italy, 2008.

Realisability Semantics For Intersection
Types and Expansion Variables
[pdf]
[slides]
[extended version]
Fairouz Kamareddine, Karim Nour, Vincent Rahli and J. B. Wells,
ITRS'08, Torino, Italy, 2008.
Technical Reports

A constraint system for a SML type error slicer
[pdf]
[BW]
Vincent Rahli, J. B. Wells and Fairouz Kamareddine
Technical Report HWMACSTR0079, HeriotWatt university, 2010

Challenges of a type error slicer for the SML language
(Obsolete, this technical report has been replaced by technical report HWMACSTR0079)
Vincent Rahli, J. B. Wells and Fairouz Kamareddine
Thesis

Thesis:
Investigations in intersection types:[submitted version] [revised version]
Confluence, and semantics of expansion in the λcalculus, and a type error slicing method