Vincent Rahli
|
|
||||||||
| Faculté ou Centre | Interdisciplinary Centre for Security, Reliability and Trust | ||||||||
| 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-060 | ||||||||
|
|||||||||
| 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
2017
Bar Induction: The Good, the Bad, and the Ugly; ;
in Abstract book of LICS 2017: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (2017)
2016
A Nominal Exploration of Intuitionism;
in The 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016) (2016)
Skalpel: A Constraint-Based Type Error Slicer for Standard ML; ; ;
in Journal of Symbolic Computation (2016)
Avoiding Leakage and Synchronization Attacks through Enclave-Side Preemption Control; ; ; ; ;
Scientific Conference (2016, December 12)
2015
Skalpel: A Type Error Slicer for Standard ML; ; ;
in Electronic Notes in Theoretical Computer Science (2015)
2014
Towards a Formally Verified Proof Assistant;
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
Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types; ;
in ITP 2013 (2013)
2012
On Realisability Semantics for Intersection Types with Expansion Variables.; ; ;
in Fundamenta Informaticae (2012), 121
2011
2010
2009
Simplified Reducibility Proofs of Church-Rosser for beta- and beta-eta-reduction;
in Electronic Notes in Theoretical Computer Science (2009), 247
2008
A Complete Realisability Semantics for Intersection Types and Arbitrary Expansion Variables; ; ;
in ICTAC 2008 (2008)
Realisability Semantics for Intersection Types and Expansion Variables; ; ;
Scientific Conference (2008)
2007
