Vincent Rahli's homepage

Vincent Rahli

Since January 2011, I am doing a Postdoc in the Nuprl group, where I am working on synthesizing and verifying distributed protocols specified in the Logic of Events, a logical framework implemented in Nuprl to reason about event structures (message sequence diagrams). We have built EventML, a ML-like programming language that cooperates with Nuprl to specify, synthesize, and verify protocols.

From October 2006 to January 2011 I was a PhD student in the School of Mathematical and Computer Sciences at Heriot-Watt University in Edinburgh.
My supervisors were Professor Fairouz Kamareddine and Doctor J. B. Wells of the ULTRA group.

[Curriculum Vitae][Publications].

Papers

	Accepted for publication On Realisability Semantics for Intersection Types with Expansion Variables [in preparation] [extended version] Fairouz Kamareddine, Karim Nour, Vincent Rahli and J. B. Wells.
	Conference papers A complete realisability semantics for intersection types and arbitrary expansion variables [pdf] [slides] [extended version] Fairouz Kamareddine, Karim Nour, Vincent Rahli and J. B. Wells, 5th International Colloquium on Theoretical Aspects of Computing (ICTAC 2008), The Marmara, Istanbul, Turkey, 1-3 September 2008. Lecture Notes in Computer Science, volume 5160, Pages 171-185. Uniform circuits, & Boolean proof net [pdf] Virgile Mogbil and Vincent Rahli, Symposium on Logical Foundations of Computer Science (LFCS'07), New York, U.S.A., June 4 - 7 2007. Lecture Notes in Computer Science, volume 4514, pages 401-421.
	Workshop papers The Logic of Events, a framework to reason about distributed systems [pdf] [slides] Mark Bickford, Vincent Rahli, and Robert L. Constable Languages for Distributed Algorithms (LADA) workshop, Philadelphia, USA, 23-24 January 2012. Simplified Reducibility Proofs of Church-Rosser for β- and βη-reduction [pdf] [slides] [extended version] Fairouz Kamareddine and Vincent Rahli Third Workshop on Logical and Semantic Frameworks, with Applications (LSFA'08), Salvador, Bahia, Brasil, 26 August 2008. Electronic Notes in Theoretical Computer Science, Volume 247, pages 85-101 Reducibility proofs in the λ-calculus [pdf] [slides] [extended version] Fairouz Kamareddine, Vincent Rahli and J. B. Wells, ITRS'08, Torino, Italy, 2008. Realisability Semantics For Intersection Types and Expansion Variables [pdf] [slides] [extended version] Fairouz Kamareddine, Karim Nour, Vincent Rahli and J. B. Wells, ITRS'08, Torino, Italy, 2008.
	Technical reports A constraint system for a SML type error slicer [pdf] [BW] Vincent Rahli, J. B. Wells and Fairouz Kamareddine Technical Report HW-MACS-TR-0079, Heriot-Watt university, 2010 Challenges of a type error slicer for the SML language (Obsolete, this technical report has been replaced by the technical report HW-MACS-TR-0079) Vincent Rahli, J. B. Wells and Fairouz Kamareddine

Talks

January 2010: Spoke about the "Type Error Slicing" project at the CS PhD seminar [slides].
May 2009: Spoke about a preliminary version of our type error slicer for SML at SPLS [slides]. This seminar was held at the University of Glasgow.
January 2009: Spoke about "Type Error Slicing" at the CS PhD seminar [slides].
September 2008: Presented our paper "A complete realisability semantics for intersection types and arbitrary expansion variables" at ICTAC 2008 , The Marmara, Istanbul, Turkey [slides].
August 2008: Second year viva [slides].
June 2008: Spoke about "Lambda-calculi and Church-Rosser property" at the CS PhD seminar [slides].
March 2008: Presented our paper "Reducibility proofs in the λ-calculus" at ITRS'08, Torino, Italy [slides].
August 2007: First year viva [slides].

Interests

During my PhD I was involved in the following projects:

	A type error slicer for SML Programming languages such as SML have sophisticated, flexible and safe type systems. Unfortunately, the type error messages for incorrect programs are confusing. promising approach to making type errors easier to understand and fix is type error slicing, in which slices (program points) containing all and only the information needed by the programmer to understand and fix a type error are identified and exhibited. We provide the following resources concerning our type error slicer: The web page of our project where you can download packages for Debian and Red-Hat-based systems as well as a web demo.
	Semantics of expansion Intersection types introduce type polymorphism in a finitary way. Expansion was introduced to recover the principal typing property in such systems. The study of realisability semantics for such systems with expansion might help casting some light on the expansion mechanism.
	Reducibility proofs Reducibility is a method based on realisability semantics where the idea is to interpret types by sets of λ-terms closed under some properties. This method seems promising in generalising diverse properties' proofs of the (typed or untyped) λ-calculus.

Thesis and reports

Thesis:
Investigations in intersection types:
Confluence, and semantics of expansion in the λ-calculus, and a type error slicing method
[submitted version] [revised version]
Second Year Report, August 2008 [pdf] [slides]. This report should be read with these articles (which are appended to the report): [44], [41], [45], [39], [42], [40].
First Year Report, August 2007 [pdf] [slides].

Tutoring

Foundations 2 (2009-2010 second semester). Taught by Doctor J. B. Wells.
Foundations 1 (2009-2010 first semester). Taught by Doctor Patrícia Vargas and Doctor J. B. Wells.
Foundations 2 (2008-2009 second semester). Taught by Doctor J. B. Wells.
Theory Bridge (2007-2008 first term): Logic (Proposition, Predicate, Boolean interpretation), Z specification, Lambda-calculus, computability. Taught by Professor Fairouz Kamareddine.
Logic and Proof (2007-2008 first term): Logic (Proposition, Predicate, Boolean interpretation, Quantification). Taught by Professor Fairouz Kamareddine.

Activities

Helper at ICFP 2009.
Member of the Organising Committee of WoLLIC 2008.

Reviewing

TYPES'07.
The Australian Journal of Logic.
LSFA'08 (Third Workshop on Logical and Semantic Frameworks, with Applications).

Contact

Email	surname at cs.cornell.edu
Address	Cornell University
	4119C Upson Hall
	Computer Science Department
	Ithaca, NY 14853
Phone	(607) 255 0110

Updated on Feb 27, 2012