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-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
Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq; ; ;
in Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq (2018, April)
2017
Validating Brouwer's Continuity Principle for Numbers Using Named Exceptions;
in Mathematical Structures in Computer Science (2017)
Bar Induction: The Good, the Bad, and the Ugly; ;
in Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (2017)
EventML: Specification, Verification, and Implementation of Crash-Tolerant State Machine Replication Systems; ; ;
in Science of Computer Programming (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
