# Marco Paviotti

## Short biography

I am currently a postdoc researcher (RA) at Imperial College
London on the Scoped Contextual
Operations and Effects
project.

I was formerly an RA at University of Kent and a
Ph.D. student at IT University of Copenhagen.

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.
(To appear)
- 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)