Startseite // SnT // People // Vincent Rahli

Vincent Rahli

Wissenschaftlicher Mitarbeiter

Fachgebiet(e) Computer science
Forschungsthemen Type theory, Programming languages, Proof assistants, Distributed computing
Fakultät oder Zentrum Interdisciplinary Centre for Security, Reliability and Trust
Postadresse Université du Luxembourg
Maison du Nombre
6, Avenue de la Fonte
L-4364 Esch-sur-Alzette
Büroadresse MNO, E02 0245-060
E-Mail
Telefon (+352) 46 66 44 6126
Fax (+352) 46 66 44 36126
Gesprochene Sprachen English, French
Forschungsaufenthalte in 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: Freitag, den 02. Dezember 2016

powered by
orbilu.uni.lu

2017

Full Text
See detailFormally Verified Differential Dynamic Logic
Bohrer, Brandon; Rahli, Vincent; Vukotic, Ivana; Volp, Marcus; Platzer, Andre

in CPP 2017 (2017)

See detailBar Induction: The Good, the Bad, and the Ugly
Rahli, Vincent; Bickford, Mark; Constable, Robert

in Abstract book of LICS 2017: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (2017)

Top of Page

2016

Full Text
See detailExercising Nuprl's Open-Endedness
Rahli, Vincent

in The 5th International Congress on Mathematical Software (2016)

Full Text
See detailA Nominal Exploration of Intuitionism
Rahli, Vincent; Bickford, Mark

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

Full Text
See detailSkalpel: A Constraint-Based Type Error Slicer for Standard ML
Rahli, Vincent; Wells, Joe; Pirie, John; Kamareddine, Fairouz

in Journal of Symbolic Computation (2016)

Full Text
See detailAvoiding Leakage and Synchronization Attacks through Enclave-Side Preemption Control
Volp, Marcus; Lackorzynski, Adam; Decouchant, Jérémie; Rahli, Vincent; Rocha, Francisco; Verissimo, Paulo

Scientific Conference (2016, December 12)

Top of Page

2015

Full Text
See detailCoq as a Metatheory for Nuprl with Bar Induction
Rahli, Vincent; Bickford, Mark

Scientific Conference (2015)

Full Text
See detailFormal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML
Rahli, Vincent; Guaspari, David; Bickford, Mark; Constable, Robert L.

in EASST (2015)

Full Text
See detailSkalpel: A Type Error Slicer for Standard ML
Rahli, Vincent; Wells, Joe B.; Pirie, John; Kamareddine, Fairouz

in Electronic Notes in Theoretical Computer Science (2015)

Top of Page

2014

Full Text
See detailA Type Theory with Partial Equivalence Relations as Types
Anand, Abhishek; Bickford, Mark; Constable, Robert L.; Rahli, Vincent

Scientific Conference (2014)

Full Text
See detailTowards a Formally Verified Proof Assistant
Anand, Abhishek; Rahli, Vincent

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)

Full Text
See detailTowards a Formally Verified Proof Assistant (technical report)
Anand, Abhishek; Rahli, Vincent

Report (2014)

Full Text
See detailA Generic Approach to Proofs about Substitution
Anand, Abhishek; Rahli, Vincent

in LFMTP 2014 (2014)

Full Text
See detailDeveloping Correctly Replicated Databases Using Formal Tools
Schiper, Nicolas; Rahli, Vincent; Van Renesse, Robbert; Bickford, Mark; Constable, Robert L.

in DSN 2014 (2014)

Top of Page

2013

Full Text
See detailFormal Program Optimization in Nuprl Using Computational Equivalence and Partial Types
Rahli, Vincent; Bickford, Mark; Anand, Abhishek

in ITP 2013 (2013)

Top of Page

2012

Full Text
See detailIntroduction to EventML
Bickford, Mark; Constable, Robert L.; Eaton, Richard; Guaspari, David; Rahli, Vincent

Report (2012)

Full Text
See detailLogic of Events, a framework to reason about distributed systems
Bickford, Mark; Constable, Robert L.; Rahli, Vincent

Scientific Conference (2012)

Full Text
See detailOn Realisability Semantics for Intersection Types with Expansion Variables.
Kamareddine, Fairouz; Nour, Karim; Rahli, Vincent; Wells, J. B.

in Fundamenta Informaticae (2012), 121

Full Text
See detailReducibility proofs in the lambda-calculus
Kamareddine, Fairouz; Rahli, Vincent; Wells, J. B.

in Fundamenta Informaticae (2012), 121

Full Text
See detailA diversified and correct-by-construction broadcast service
Rahli, Vincent; Schiper, Nicolas; Renesse, Robbert Van; Bickford, Mark; Constable, Robert L.

in ICNP 2012 (2012)

Full Text
See detailShadowDB: A Replicated Database on a Synthesized Consensus Core
Schiper, Nicolas; Rahli, Vincent; Renesse, Robbert Van; Bickford, Mark; Constable, Robert L.

in HotDep 2012 (2012)

Top of Page

2011

Top of Page

2010

Full Text
See detailA constraint system for a SML type error slicer
Rahli, Vincent; Wells, J. B.; Kamareddine, Fairouz

Report (2010)

Top of Page

2009

Full Text
See detailSimplified Reducibility Proofs of Church-Rosser for beta- and beta-eta-reduction
Kamareddine, Fairouz; Rahli, Vincent

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

Top of Page

2008

Full Text
See detailA Complete Realisability Semantics for Intersection Types and Arbitrary Expansion Variables
Kamareddine, Fairouz; Nour, Karim; Rahli, Vincent; Wells, J. B.

in ICTAC 2008 (2008)

Full Text
See detailRealisability Semantics for Intersection Types and Expansion Variables
Kamareddine, Fairouz; Nour, Karim; Rahli, Vincent; Wells, J. B.

Scientific Conference (2008)

Full Text
See detailReducibility Proofs in the λ-Calculi with Intersection Types
Kamareddine, Fairouz; Rahli, Vincent; Wells, J. B.

Scientific Conference (2008)

Top of Page

2007

Full Text
See detailUniform Circuits & Boolean Proof Nets
Mogbil, Virgile; Rahli, Vincent

in LFCS 2007 (2007)

Top of Page