I am currently a postdoc researcher (RA) at Imperial College
London on the Scoped Contextual
Operations and Effects
project and Visiting Researcher at University of Kent. I was formerly an RA at University of Kent and a
Ph.D. student at IT University of Copenhagen.

Contacts : @

Thesis dissertation : Denotational Semantics in Synthetic Guarded
Domain Theory

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

Publications

M. Paviotti, S. Cooksey, A. Paradis, D. Wright, S. Owens and M. Batty. Modular Relaxed Dependencies in Weak Memory Concurrency. ESOP 2020.
(paper)

M. Batty, S. Cooksey, S. Owens, A. Paradis, M. Paviotti and D. Wright. Modular Relaxed Dependencies: A new approach to the
Out-Of-Thin-Air Problem. C++ ISO Draft Proposal,
2019-10-15. (draft)

R.E. Møgelberg and M. Paviotti. Denotational semantics of recursive types in
Synthetic guarded domain theory. MSCS, 2019. (paper)

M. Paviotti and J. Bengtson. Formally Verifying Exceptions
for Low-level code with Separation Logic. JLAMP, 2018.
(code)
(paper)

M. Paviotti. Denotational semantics in Synthetic guarded domain theory. Ph.D. thesis, IT University of Copenhagen, 2016.
(thesis)
(bibtex)
(slides)

R.E. Møgelberg and M. Paviotti. Denotational semantics of recursive types in
Synthetic guarded domain theory. LICS 2016.
(paper)
(slides)

M. Paviotti, R.E. Møgelberg, and L. Birkedal. A
model of PCF in Guarded Type Theory. MFPS
2015. (slides)
(paper)

M. Paviotti and J. Bengtson. Formally Verifying Exceptions for Low-level code
with Separation Logic. NWPT 2015.
(code)
(slides)
(paper)

M. Miculan, M. Paviotti. Synthesis of distributed mobile programs
using monadic types in Coq. ITP 2012.
(code)
(slides)
(paper)

Unpublished

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