Conference and Journal Papers
-
Separating Markov's Principles
[pdf]
In collaboration with Liron Cohen, Yannick Forster, Dominik Kirst, and Bruno da Rocha Paiva,
LICS 2024
-
OneShot: View-Adapting 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 Event-Triggered Real-Time Byzantine-Resilient 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]
In collaboration with Mark Bickford, Liron Cohen, and Robert L. Constable
JACM, 2019
-
A Verified Theorem Prover Backend Supported by a Monotonic Library
[pdf]
[Github]
In collaboration with Liron Cohen, and Mark Bickford
LPAR 2018
-
Computability Beyond Church-Turing via Choice Sequences
[pdf]
[extended version]
[Github]
In collaboration with Liron Cohen, Mark Bickford and Robert L. Constable
LICS 2018
-
Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq
[pdf]
[Github]
In collaboration with Ivana Vukotic, Marcus Volp, and Paulo Verissimo
ESOP 2018
-
Validating Brouwer's Continuity Principle for Numbers Using Named Exceptions
[pdf]
[Github]
In collaboration with Mark Bickford
MSCS, 2017
-
Bar Induction: The Good, the Bad, and the Ugly
[pdf]
[extended version]
[Github]
In collaboration with Mark Bickford and Robert L. Constable
LICS 2017
-
Formally Verified Differential Dynamic Logic
[pdf]
[Github]
In collaboration with Brandon Bohrer, 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
Crash-Tolerant State Machine Replication Systems
[pdf]
[Github]
In collaboration with David Guaspari, Mark Bickford, and Robert L. Constable
Science of Computer Programming journal, 2017
-
Exercising Nuprl's Open-Endedness
[pdf]
Vincent Rahli
The 5th International Congress on Mathematical Software (ICMS 2016)
-
A Nominal Exploration of Intuitionism
[pdf]
[Github]
In collaboration with Mark Bickford
The 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016).
-
Skalpel: A Constraint-Based Type Error Slicer for Standard ML
[pdf]
[Github]
In collaboration with 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]
In collaboration with Abhishek Anand
5th Conference on Interactive Theorem Proving (ITP 2014).
-
Developing Correctly Replicated Databases Using Formal Tools
[pdf]
[Github]
In collaboration with Nicolas Schiper, 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]
In collaboration with Mark Bickford, and Abhishek Anand
4th Conference on Interactive Theorem Proving (ITP 2013), Rennes, France, 22-26 July 2013.
-
On Realisability Semantics for Intersection Types with Expansion Variables
[pdf]
In collaboration with Fairouz Kamareddine, Karim Nour, and J. B. Wells
Fundamenta Informaticae, volume 121, 2012
-
Reducibility proofs in the λ-calculus
[pdf]
In collaboration with Fairouz Kamareddine, and J. B. Wells
Fundamenta Informaticae, volume 121, 2012 -
A complete realisability semantics for intersection
types and arbitrary expansion variables
[pdf]
[slides]
[extended version]
In collaboration with Fairouz Kamareddine, Karim Nour, and J. B. Wells
5th International Colloquium on Theoretical Aspects of Computing (ICTAC 2008), The Marmara, Istanbul, Turkey, 1-3 September 2008.
Lecture Notes in Computer Science, volume 5160, Pages 171-185.
-
Uniform circuits, & Boolean proof net
[pdf]
In collaboration with Virgile Mogbil
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 401-421.
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 Fault-Tolerant 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 Correct-by-Construction 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, 23-24 January 2012.
-
Simplified Reducibility Proofs of Church-Rosser
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 85-101
-
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 HW-MACS-TR-0079, Heriot-Watt university, 2010
-
Challenges of a type error slicer for the SML language
(Obsolete, this technical report has been replaced by technical report HW-MACS-TR-0079)
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