Vincent Rahli
![]() |
|
||||||||
Faculté ou Centre | Interdisciplinary Centre for Security, Reliability and Trust | ||||||||
Unité de recherche | SnT | ||||||||
Adresse postale |
Université du Luxembourg Maison du Nombre 6, Avenue de la Fonte L-4364 Esch-sur-Alzette |
||||||||
Bureau sur le campus | MNO, E02 0245-020 | ||||||||
![]() |
|||||||||
Téléphone | (+352) 46 66 44 6126 | ||||||||
Fax | (+352) 46 66 44 36126 | ||||||||
Langues parlées | English, French | ||||||||
Séjours de recherche en | France, Luxembourg, United Kingdom, USA | ||||||||
I received a PhD in computer science from Heriot-Watt University in Edinburgh, Scotland, in January 2011. My thesis was supervised by Prof. Fairouz Kamareddine and Dr. Joe B. Wells, and was about the theory and applications of intersection type systems. During my PhD, I among other things built a type error slicer for SML. More information can be found here: http://www.macs.hw.ac.uk/ultra/skalpel/.
From 2011 to 2015 I was a research associate at Cornell University, NY, USA, where I was working in the PRL group led by Prof. Robert L. Constable on discovering and perfecting mathematically sound programming tools such as proof assistants, for building highly trustworthy systems. During my stay at Cornell, with the guidance of Dr. Mark Bickford and Rich Eaton, I quickly became a happy Nuprl user and designer. More information can be found here: http://www.nuprl.org/. We among other things, verified Nuprl in Coq. More information can be found here: http://www.nuprl.org/html/Nuprl2Coq/. We were also working on distributed systems, and successfully specified, verified, and synthesized Multi-Paxos using Nuprl (see our DSN2014 paper).
Since September 2015, I'm a member of the CritiX research group led by Prof. Paulo Verissimo. More information can be found here: https://wwwen.uni.lu/snt/research/critix/. I'm working on the verification of fault-tolerant distributed systems.
My research interests include programming languages, type theory, distributed systems, and proof assistants.
Last updated on: vendredi 02 décembre 2016

2018

; ; ;
Scientific Conference (2018)
2017

;
in Mathematical Structures in Computer Science (2017)

; ;
in Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (2017)

; ; ;
in Science of Computer Programming (2017)
2016

;
in The 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016) (2016)

; ; ;
in Journal of Symbolic Computation (2016)

; ; ; ; ;
Scientific Conference (2016, December 12)
2015

; ; ;
in Electronic Notes in Theoretical Computer Science (2015)
2014

;
in Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings (2014)
2013

; ;
in ITP 2013 (2013)
2012

; ; ;
in Fundamenta Informaticae (2012), 121
2011
2010
2009

;
in Electronic Notes in Theoretical Computer Science (2009), 247
2008

; ; ;
in ICTAC 2008 (2008)

; ; ;
Scientific Conference (2008)