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
First steps in denotational semantics for weak memory concurrency
Draft.
Marco Paviotti, Mark Batty and Scott Owens
Formally Verifying Exceptions for Lowlevel code with Separation Logic
Journal of Logical and Algebraic Methods in
Programming. JLAMP, 2018.
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 Lowlevel 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
