Who am I?
I am a postdoctoral researcher at UPenn, working on security for the CRASH/SAFE project, under the direction of Benjamin Pierce.
Before that, I was Ph.D. student in the Gallium team, at INRIA Paris-Rocquencourt. My advisor was Didier Rémy, I was working on module systems, type abstraction, generativity, and singleton kinds.
News
- October 2012: Release of the mechanized verification in Coq of the paper Robust declassification by Steve Zdancewicz and Andrew C. Myers.
- July 2012: submitted a draft paper entitled A Theory on Information-Flow Labels.
- October 2011: Paper accepted at the PLOS'11 Workshop (Cascais, Portugal) Preliminary Design of the SAFE Platform. The slides of the talk I gave are available.
- December 2010: Release of the Fzip typechecker: a typechecker for an explicitly typed language supporting polymorphism, open existential types, singleton kinds and subtyping.
- December 2010: I successfully defended my thesis, entitled "Programming with first-class modules in a core language with subtyping, singleton kinds and open existential types". The manuscript and the slides are online!
- September 2010: The slides of my talk at WMM'10 are online! The submitted short abstract is also available for some more details.
- April 2010: A mechanized proof of soundness for System FzipCore, using the Coq proof assistant (version 8.2pl1), with the great help of the tools Ott and LNgen. [Sources | Html]
- August 2009: Some results on the combination of relations (confluence, well-foundedness), formalized in Coq (version 8.2-1). Main lemmas are Hindley-Rosen's, Akama's and Di Cosmo-Piperno-Geser's condition. [Sources | Html]
