Short biography

I am currently a postdoc researcher at University of Kent (England) working with Scott Owens on relaxed memory models. I have received my Ph.D. at IT University of Copenhagen (Denmark) in 2016 under the supervision of Rasmus Møgelberg and Jesper Bengtson.

Thesis dissertation : Denotational Semantics in Synthetic Guarded Domain Theory

Keywords: semantics of programming languages, mathematical logic, category theory and type theory.

Publications

  • Formally Verifying Exceptions for Low-level code with Separation Logic
    Journal of Logical and Algebraic Methods in Programming (JLAMP). To appear, 2017.
    M. Paviotti and J. Bengtson
  • Denotational semantics of recursive types in Synthetic guarded domain theory
    Journal version submitted to MSCS, 2017.
    R.E. Møgelberg and M. Paviotti
  • Denotational semantics in Synthetic guarded domain theory
    Ph.D. thesis, IT University of Copenhagen, 2016.
    M. Paviotti
  • Denotational semantics of recursive types in Synthetic guarded domain theory
    Logic in Computer Science, LICS 2016.
    R.E. Møgelberg and M. Paviotti
  • A model of PCF in Guarded Type Theory
    In Electronic Notes in Theorerical Computer Science, 2015. (MFPS 2015).
    M. Paviotti, R.E. Møgelberg, and L. Birkedal
  • Formally Verifying Exceptions for Low-level code with Separation Logic
    27th Nordic Workshop on Programming Theory, 2015. (NWPT 2015).
    M. Paviotti and J. Bengtson
    • Synthesis of distributed mobile programs using monadic types in Coq
      In Proceedings of the 3rd International Conference on Interactive Theorem Proving, 2012.
      (ITP 2012).
      M. Miculan, M. Paviotti

    Unpublished

    • Extraction of certified programs with effects from proofs with monadic types in Coq
      Manuscript, 2013.
      M. Miculan, M. Paviotti

    valid XHTML | CSS