Dr Vincent Rahli PhD

Dr Vincent Rahli

School of Computer Science
Senior Lecturer

Contact details

Address
School of Computer Science
University of Birmingham
Edgbaston
Birmingham
B15 2TT
UK

Dr Vincent Rahli is a Senior Lecturer in Computer Science at the Univeristy of Birmingham and is a member of the Theory of Computation research group. 

He is broadly interested in type theory (especially in constructive and intuitionistic theories) and in distributed computing (especially in the foundations and verification of fault-tolerant systems).

Please follow the link below to find out more about Vincent's work:

Dr Vincent Rahli - personal web page

Qualifications

PhD in Computer Science 2011

Biography

Vincent obtained a PhD in Computer Science from Heriot-Watt University in Edinburg, Scotland, UK in 2011. During his PhD, Vincent studied both the foundations and applications of intersection type systems.

After his PhD, Vincent went on to do a postdoc within the PRL group at Cornell, USA. There, he had the opportunity to learn from amazing colleagues about topics that became his passion, such as intuitionism, formal verification, and distritributed systems.

He then had the opportunity to contribute significantly to these topics while he was a Research Associate, within the CritiX system group in Luxembourg from 2015 to 2019.

 Finally, since July 2019, Vincent is back in the UK, working as a Senior Lecturer at the University of Birmingham

Teaching

Computer Aided Verification, Spring 2020

Research

  • Intuitionistic type theory

  • Theorem proving

  • Formal verification of distributed systems

  • Real-time fault-tolerant systems

Publications

Recent publications

Article

Kozhaya, D, Decouchant, J, Rahli, V & Veríssimo, PJE 2021, 'PISTIS: an event-triggered real-time Byzantine-resilient protocol suite', IEEE Transactions on Parallel and Distributed Systems. https://doi.org/10.1109/TPDS.2021.3056718

Rahli, V, Bickford, M, Cohen, L & Constable, RL 2019, 'Bar induction is compatible with constructive type theory', Journal of the ACM, vol. 66, no. 2, pp. 13:1-13:35. https://doi.org/10.1145/3305261

Rahli, V & Bickford, M 2018, 'Validating Brouwer's continuity principle for numbers using named exceptions', Mathematical Structures in Computer Science, vol. 28, no. 6, pp. 942-990. https://doi.org/10.1017/S0960129517000172

Rahli, V, Guaspari, D, Bickford, M & Constable, RL 2017, 'EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems', Science of Computer Programming, vol. 148, pp. 26-48. https://doi.org/10.1016/j.scico.2017.05.009

Conference article

Bickford, M, Cohen, L, Constable, RL & Rahli, V 2021, 'Open bar - a Brouwerian intuitionistic logic with a pinch of excluded middle', Leibniz International Proceedings in Informatics, vol. 183, pp. 11:1-11:23. https://doi.org/10.4230/LIPIcs.CSL.2021.11

Vukotic, I, Rahli, V & Veríssimo, PJE 2019, 'Asphalion: trustworthy shielding against Byzantine faults', Proceedings of the ACM on Programming Languages, vol. 3, no. OOPSLA, 138. https://doi.org/10.1145/3360564

Conference contribution

Cohen, L & Rahli, V 2022, Constructing Unprejudiced Extensional Type Theories with Choices via Modalities. in FSCD 2022.

Decouchant, J, Kozhaya, D, Rahli, V & Yu, J 2022, Damysus: streamlined BFT consensus leveraging trusted components. in EuroSys 2022 - Proceedings of the 17th European Conference on Computer Systems: Proceedings of the Seventeenth European Conference on Computer Systems. Association for Computing Machinery (ACM), pp. 1-16, EuroSys '22, Rennes, France, 5/04/22. https://doi.org/10.1145/3492321.3519568

Bonomi, S, Decouchant, J, Farina, G, Rahli, V & Tixeuil, S 2021, Practical Byzantine reliable broadcast on partially connected networks. in 2021 IEEE 41st International Conference on Distributed Computing Systems (ICDCS)., 9546451, Proceedings of the International Conference on Distributed Computing Systems, IEEE, pp. 506-516, 2021 IEEE 41st International Conference on Distributed Computing Systems, Washington DC, Washington, United States, 7/07/21. https://doi.org/10.1109/ICDCS51616.2021.00055

Rahli, V, Cohen, L & Bickford, M 2018, A verified theorem prover backend supported by a monotonic library. in G Barthe, G Sutcliffe & M Veanes (eds), LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol. 57, EasyChair Publications, pp. 564-582, LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 17/11/18. https://doi.org/10.29007/f58n

Bickford, M, Cohen, L, Constable, RL & Rahli, V 2018, Computability beyond Church-Turing via choice sequences. in LICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. Association for Computing Machinery (ACM), pp. 245-254, 33rd Annual ACM/IEEE Symposium on Logic in Computer Science , Oxford, United Kingdom, 9/07/18. https://doi.org/10.1145/3209108.3209200

Rahli, V, Vukotic, I, Völp, M & Veríssimo, PJE 2018, Velisarios: Byzantine fault-tolerant protocols powered by Coq. in A Ahmed (ed.), Programming Languages and Systems : 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10801, Springer, pp. 619-650, 27th European Symposium on Programming, ESOP 2018, Thessaloniki, Greece, 14/04/18. https://doi.org/10.1007/978-3-319-89884-1_22

Rahli, V, Bickford, M & Constable, RL 2017, Bar induction: The good, the bad, and the ugly. in 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017. Institute of Electrical and Electronics Engineers (IEEE), 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017), Reykjavik, Iceland, 20/06/17. https://doi.org/10.1109/LICS.2017.8005074

Bohrer, B, Rahli, V, Vukotic, I, Völp, M & Platzer, A 2017, Formally verified differential dynamic logic. in Y Bertot & V Vafeiadis (eds), Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017. Association for Computing Machinery (ACM), pp. 208-221, 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, 16/01/17. https://doi.org/10.1145/3018610.3018616

Veríssimo, PJE, Völp, M, Decouchant, J, Rahli, V & Rocha, F 2017, Meeting the challenges of critical and extreme dependability and security. in DS Kim, M Kitakami & V Varadharajan (eds), 22nd IEEE Pacific Rim International Symposium on Dependable Computing, PRDC 2017. Institute of Electrical and Electronics Engineers (IEEE), pp. 92-97, 22nd IEEE Pacific Rim International Symposium on Dependable Computing, PRDC 2017, Christchurch, New Zealand, 22/01/17. https://doi.org/10.1109/PRDC.2017.21

View all publications in research portal