Cluny (France), 2012

Welcome to my academic homepage. I am a former research and teaching assistant at EPFL (left in late 2006).

I am from France and did my scolarship in the universities of Lyon, Nancy and Paris. In early 2001 I went to Switzerland to start a Ph.D. in Computer Science at the Ecole Polytechnique Fédérale de Lausanne.

I received the diploma in late 2006. In my Ph.D. I formalized and proved sound a central part of the type system of Scala, an object-oriented programming language designed by my supervisor Martin Odersky and developped in his Programming Methods Laboratory.

• Adding Type Constructor Parameterization to Java. Vincent Cremet, Philippe Altherr. In Journal of Object Technology, vol. 7, no. 5, Special Issue: Workshop on FTfJP, ECOOP'07, June 2008, pp.25-65, http://www.jot.fm/issues/issue_2008_06/article2/ . (bib), (pdf), (homepage). (A previous version was presented at the FTfJP'07 ECOOP workshop).
• A Soundness Proof of Virtual Types Formalized in Coq. Vincent Cremet, Complete formalization of the proofs presented in my PhD thesis, August 2006. (Download the proof), (README), (Online documentation).
• A Core Calculus for Scala Type Checking. Vincent Cremet, François Garillot, Sergueï Lenglet and Martin Odersky. Proceedings of MFCS 06 (invited talk), August 2006. (bib), (pdf).
• Foundations for Scala: Semantics and Proof of Virtual Types. Vincent Cremet. PhD thesis, EPFL, No. 3556, May 2006. (bib), (ps), (pdf, exported from ps, 74 Mo). Slides in French : for printing (pdf), for talk (pdf).
• Inner Classes and Virtual Types. Philippe Altherr, Vincent Cremet. EPFL Technical Report IC/2005/013, March 2005 . (bib), (pdf).
• PiLib: A Hosted Language for Pi-calculus Style Concurrency. Vincent Cremet, Martin Odersky. Dagstuhl proceedings: Domain-Specific Program Generation, 2003. (bib), (pdf).
• An Equational Theory for Transactions. Andrew P. Black, Vincent Cremet, Rachid Guerraoui and Martin Odersky. 23rd Conference on Foundations of Software Technology and Theoretical Computer Science, Mumbai (Bombay), India, December 2003. (bib), (pdf). Technical report: (pdf).
• A Nominal Theory of Objects with Dependent Types. Martin Odersky, Vincent Cremet, Christine Roeckl and Matthias Zenger. Proc. ECOOP'03, July 2003. (bib), (pdf). Technical report: (pdf).
• Spécification et vérification de systèmes temps-réel avec la logique linéaire. Vincent Cremet, supervised by Mitsuhiro Okada and Jean-Pierre Jouannaud. Diploma thesis (D.E.A de Programmation: Sémantique, Preuves et Langages, Université Paris 7-Denis Diderot), 2000. (bib), (ps), (pdf, exported from ps, 33 Mo).

At EPFL, I have been a teaching assistant in the following courses.

• Compilation (in parentheses the name of the implemented language). Winter semesters 2001 (FuLL), 2002 (Misc), 2003 (Misc), 2004 (Eins) and 2005 (Zwei).
• Programmation IV (Study of programming paradigms). Summer semesters 2002, 2003, 2004 and 2005.
• Concurrency: Languages, Programming and Theory. Winter semesters 2002 and 2003 (use of the PiLib Scala Library).
• Advanced Topics in Programming Languages and Concurrency (AToPLaC). Summer semester 2003.
• Informatique II. Summer semester 2001 (C++).

During my PhD at EPFL I defined and supervised two student semester projects.

• Generating Typing Proofs for Scaletta. Grégory Mermoud. Semester Project, June 2005. (pdf).
• Recherche d'information dans un programme Scala. Roland Tchakoute. Semester Project, February 2004. (pdf).

• Scaladoc. I have been the main developer of Scaladoc, a Javadoc-like documentation generator for Scala, until Scala reached version 2. In this project, I have been assisted by Stéphane Micheloud.

• Preuve de l'énigme du Sphinx. 2003. (pdf).
• A proof of the confluence of combinatory logic in Coq. 2003. There is a version without the proofs and another one with the proofs.
• A proof of the undecidability of the halting problem in Coq. 2003. There is a version without the proofs and another one with the proofs.
• A proposition to quickly integrate join definitions in Scala. 2003. (homepage).