Vincent Rahli

Vincent Rahli is a Senior Lecturer (Associate Professor) at the School of Computer Science, University of Birmingham, where he has been working since July 2019. Prior to this position, he was a Research Associate in the CritiX group led by Prof. Paulo Verissimo at SnT in Luxembourg from September 2015 to May 2019, working on verification of distributed systems and intuitionistic type theory. Before that, he was a postdoc and Research Associate in the PRL group led by Prof. Robert L. Constable at Cornell University from January 2011 to July 2015, working with the Nuprl proof assistant. He completed his PhD at Heriot-Watt University in Edinburgh under the supervision of Prof. Fairouz Kamareddine and Dr. J. B. Wells.

Vincent's research interests span several interconnected areas of theoretical computer science and formal methods:

• Formal verification of distributed systems, particularly Byzantine fault-tolerant protocols
• Intuitionistic and nominal type theory, including Brouwer's continuity principles
• Development and verification of proof assistants like Nuprl and Coq
• EventML: a specification language for verified distributed protocols
• Theoretical foundations of programming languages and logic

His recent publications demonstrate a strong focus on bridging theoretical foundations with practical verification of distributed systems. He has made significant contributions to formalizing Brouwer's continuity principles in type theory while simultaneously applying these theoretical insights to verify real-world distributed protocols. His work often combines deep theoretical results in constructive mathematics with practical implementations in proof assistants like Coq and Nuprl.

He has received recognition for his work through publications in top-tier conferences including POPL, LICS, CSL, and OOPSLA. His research has been applied to verify important distributed protocols such as Paxos variants and Byzantine fault-tolerant consensus algorithms.

He has collaborated with numerous researchers including Liron Cohen, Mark Bickford, Robert L. Constable, Paulo Verissimo, and others. His work on Velisarios and Asphalion provides frameworks for verifying Byzantine fault-tolerant and hybrid fault-tolerant systems.