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

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

Rahli, V, Wells, JB, Pirie, J & Kamareddine, F 2017, 'Skalpel: A constraint-based type error slicer for Standard ML', Journal of Symbolic Computation, vol. 80, pp. 164-208. https://doi.org/10.1016/j.jsc.2016.07.013

Rahli, V, Guaspari, D, Bickford, M & Constable, RL 2015, 'Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML', Electronic Communications of the EASST, vol. 72. https://doi.org/10.14279/tuj.eceasst.72.1013

Conference contribution

Vukotic, I, Rahli, V & Veríssimo, PJE 2019, Asphalion: Trustworthy Shielding Against Byzantine Faults. in SPLASH 2019 OOPSLA.

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

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

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

Völp, M, Lackorzynski, A, Decouchant, J, Rahli, V, Rocha, F & Veríssimo, PJE 2016, Avoiding leakage and synchronization attacks through enclave-side preemption control. in Proceedings of the 1st Workshop on System Software for Trusted Execution, SysTEX@Middleware 2016, Trento, Italy, December 12, 2016., 6, Association for Computing Machinery (ACM), pp. 6:1-6:6. https://doi.org/10.1145/3007788.3007794

Rahli, V 2016, Exercising Nuprl's open-endedness. in G-M Greuel, T Koch, P Paule & A Sommese (eds), Mathematical Software - ICMS 2016 : 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9725, Springer, pp. 18-27, The 5th International Congress on Mathematical Software, ICMS 2016, Berlin, Germany, 11/07/16. https://doi.org/10.1007/978-3-319-42432-3_3

Rahli, V & Bickford, M 2016, A nominal exploration of intuitionism. in Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016. Association for Computing Machinery (ACM), pp. 130-141, 5th ACM SIGPLAN Conference on Certified Programs and Proofs, St. Petersburg, FL, United States, 18/01/16. https://doi.org/10.1145/2854065.2854077

View all publications in research portal