Dr Vincent Rahli PhD

Dr Vincent Rahli

School of Computer Science
Senior Lecturer
Head of Quality of Computer Science

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, vol. 32, no. 9, 9347806, pp. 2277-2290. 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, a13, 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

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

Decouchant, J, Kozhaya, D, Rahli, V & Yu, J 2024, OneShot: View-Adapting Streamlined BFT Protocols with Trusted Execution Environments. in 2024 IEEE International Symposium on Parallel and Distributed Processing (IPDPS). International Symposium on Parallel and Distributed Processing (IPDPS), IEEE, 38th IEEE International Symposium on Parallel and Distributed Processing (IPDPS), San Francisco, United States, 27/05/24.

Cohen, L, Da Rocha Paiva, B, Rahli, V & Tosun, A 2023, Inductive Continuity via Brouwer Trees. in J Leroux, S Lombardy & D Peleg (eds), 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics, vol. 272, Schloss Dagstuhl, pp. 37:1-37:16, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023), Bordeaux, France, 28/08/23. https://doi.org/10.4230/LIPIcs.MFCS.2023.37

Cohen, L & Rahli, V 2023, Realizing Continuity Using Stateful Computations. in B Klin & E Pimentel (eds), 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics, vol. 252, Schloss Dagstuhl, pp. 15:1-15:18, 31st EACSL Annual Conference on Computer Science Logic, CSL 2023, Warsaw, Poland, 13/02/23. https://doi.org/10.4230/LIPIcs.CSL.2023.15

Cohen, L & Rahli, V 2022, Constructing unprejudiced extensional type theories with choices via modalities. in AP Felty (ed.), 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)., 10, Leibniz International Proceedings in Informatics, vol. 228, Schloss Dagstuhl, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), Haifa, Israel, 2/08/22. https://doi.org/10.4230/LIPIcs.FSCD.2022.10

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

View all publications in research portal