Who am I?
- February 2013: submitted a draft paper entitled A Theory on Information-Flow Labels with its corresponding Coq development.
- October 2012: Release of the mechanized verification in Coq of the paper Robust declassification by Steve Zdancewicz and Andrew C. Myers.
- 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]