About

I am an Assistant Professor of Computer Science at the Department of Mathematics and Computer Science of the University of Southern Denmark, member of the Section of Artificial Intelligence, Cybersecurity, and Programming Languages.

My research mission is to make it more effective and robust to program and analyse concurrent systems. An overarching theme of my research approach is the use of formal methods and programming languages techniques as well as the aim for a unifying mathematical perspective rooted in Logic and Category Theory.

Office: Ø16-601a-2
Address: Campusvej 55, 5230 Odense M, Denmark"
Email: peressotti@sdu.dk
Phone: +45 65 50 90 26

Highlights

Feb'21
I will serve in the PC of the 2nd International Workshop on Agility with Microservices Programming (AMP 2021) at XP 2021.
Oct'20
I gave a lecture about Formal Methods at CyberSecurity Days 2020, a seminar funded by the Centre for Cyber Security of the Danish Ministry of Defence to promote IT security.
Sep'20
I gave the talk "A logical reconstruction of the π-calculus and its behavioural theory" at the Formal Methods Seminar of the Technical University of Warsaw, PL.
Aug'20
I gave a lecture about Formal Methods and a tutorial on TLA+ at the Danish Summer School on CyberSecurity.
Aug'20
I gave an invited talk about programming multiparty protocols with Choral at the International Conference on The Future of Standards in CyberSecurity.
Jun'20
We released the first beta of Choral, a Java-like programming language for type-safe multiparty protocols. Choral is based on our paper "Choreographies as Objects".

All news

Selected publications

Giallorenzo, S., Montesi, F., Peressotti, M., Richter, D., Salvaneschi, G. and Weisenburger, P. 2021. Multiparty Languages: The Choreographic and Multitier Cases. 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 12-17, 2021, Aarhus, Denmark (Virtual Conference) (2021).
Choreographic languages aim to express multiparty communication protocols, by providing primitives that make interaction manifest. Multitier languages enable programming computation that spans across several tiers of a distributed system, by supporting primitives that allow computation to change the location of execution. Rooted into different theoretical underpinnings—respectively process calculi and lambda calculus—the two paradigms have been investigated independently by different research communities with little or no contact. As a result, the link between the two paradigms has remained hidden for long. In this paper, we show that choreographic languages and multitier languages are surprisingly similar. We substantiate our claim by isolating the core abstractions that differentiate the two approaches and by providing algorithms that translate one into the other in a straightforward way. We believe that this work paves the way for joint research and cross-fertilisation among the two communities.
@inproceedings{GMPRSW21,
  author = {Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Richter, David and Salvaneschi, Guido and Weisenburger, Pascal},
  title = {Multiparty Languages: The Choreographic and Multitier Cases},
  booktitle = {35th European Conference on Object-Oriented Programming, {ECOOP} 2021, July 12-17, 2021, Aarhus, Denmark (Virtual Conference)},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  year = {2021},
  pubstate = { forthcoming }
}
Cruz-Filipe Luı́s, Montesi, F. and Peressotti, M. 2021. Formalising a Turing-Complete Choreographic Language in Coq. 12th International Conference on Interactive Theorem Proving, ITP 2021, 29 June – 01 July,September 9-12, 2021, Rome, IT (2021).
Theory of choreographic languages typically includes a number of complex results that are proved by structural induction. The high number of cases and the subtle details in some of them lead to long reviewing processes, and occasionally to errors being found in published proofs. In this work, we take a published proof of Turing completeness of a choreographic language and formalise it in Coq. Our development includes formalising the choreographic language and its basic properties, Kleene’s theory of partial recursive functions, the encoding of these functions as choreographies, and proving this encoding correct. With this effort, we show that theorem proving can be a very useful tool in the field of choreographic languages: besides the added degree of confidence that we get from a mechanised proof, the formalisation process led us to a significant simplification of the underlying theory. Our results offer a foundation for the future formal development of choreographic languages.
@inproceedings{CMP21,
  author = {Cruz{-}Filipe, Lu{\'{\i}}s and Montesi, Fabrizio and Peressotti, Marco},
  editor = {Cohen, Liron and Kaliszyk, Cezary},
  title = {Formalising a Turing-Complete Choreographic Language in Coq},
  booktitle = {12th International Conference on Interactive Theorem Proving, {ITP} 2021, 29 June – 01 July,September 9-12, 2021, Rome, {IT}},
  series = {LIPIcs},
  volume = {193},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  year = {2021},
  pubstate = { forthcoming }
}
Kokke, W., Montesi, F. and Peressotti, M. 2019. Better late than never: a fully-abstract semantics for classical processes. PACMPL. 3, POPL (2019), 24:1–24:29. DOI:10.1145/3290337.
We present Hypersequent Classical Processes (HCP), a revised interpretation of the “Proofs as Processes” correspondence between linear logic and the π-calculus initially proposed by Abramsky [1994], and later developed by Bellin and Scott [1994], Caires and Pfenning [2010], and Wadler [2014], among others. HCP mends the discrepancies between linear logic and the syntax and observable semantics of parallel composition in the π-calculus, by conservatively extending linear logic to hyperenvironments (collections of environments, inspired by the hypersequents by Avron [1991]). Separation of environments in hyperenvironments is internalised by ⊗ and corresponds to parallel process behaviour. Thanks to this property, for the first time we are able to extract a labelled transition system (lts) semantics from proof rewritings. Leveraging the information on parallelism at the level of types, we obtain a logical reconstruction of the delayed actions that Merro and Sangiorgi [2004] formulated to model non-blocking I/O in the π-calculus. We define a denotational semantics for processes based on Brzozowski derivatives, and uncover that non-interference in HCP corresponds to Fubini’s theorem of double antiderivation. Having an lts allows us to validate HCP using the standard toolbox of behavioural theory. We instantiate bisimilarity and barbed congruence for HCP, and obtain a full abstraction result: bisimilarity, denotational equivalence, and barbed congruence coincide.
@article{KMP19,
  author = {Kokke, Wen and Montesi, Fabrizio and Peressotti, Marco},
  title = {Better late than never: a fully-abstract semantics for classical processes},
  journal = {{PACMPL}},
  volume = {3},
  number = {{POPL}},
  pages = {24:1--24:29},
  year = {2019},
  url = {https://doi.org/10.1145/3290337},
  doi = {10.1145/3290337}
}
Brengos, T. and Peressotti, M. 2019. Behavioural equivalences for timed systems. Logical Methods in Computer Science. 15, 1 (2019). DOI:10.23638/LMCS-15(1:17)2019.
Timed transition systems are behavioural models that include an explicit treatment of time flow and are used to formalise the semantics of several foundational process calculi and automata. Despite their relevance, a general mathematical characterisation of timed transition systems and their behavioural theory is still missing. We introduce the first uniform framework for timed behavioural models that encompasses known behavioural equivalences such as timed bisimulations, timed language equivalences as well as their weak and time-abstract counterparts. All these notions of equivalences are naturally organised by their discriminating power in a spectrum. We prove that this result does not depend on the type of the systems under scrutiny: it holds for any generalisation of timed transition system. We instantiate our framework to timed transition systems and their quantitative extensions such as timed probabilistic systems.
@article{BP19,
  author = {Brengos, Tomasz and Peressotti, Marco},
  title = {Behavioural equivalences for timed systems},
  journal = {Logical Methods in Computer Science},
  volume = {15},
  number = {1},
  year = {2019},
  url = {https://doi.org/10.23638/LMCS-15(1:17)2019},
  doi = {10.23638/LMCS-15(1:17)2019}
}
Brengos, T. and Peressotti, M. 2016. A Uniform Framework for Timed Automata. 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada (2016), 26:1–26:15.
Timed automata, and machines alike, currently lack a general mathematical characterisation. In this paper we provide a uniform coalgebraic understanding of these devices. This framework encompasses known behavioural equivalences for timed automata and paves the way for the extension of these notions to new timed behaviours and for the instantiation of established results from the coalgebraic theory as well. Key to this work is the use of lax functors for they allow us to model time flow as a context property and hence offer a general and expressive setting where to study timed systems: the index category encodes ḧow step sequences form executions\" (e.g. whether steps duration get accumulated or kept distinct) whereas the base category encodes s̈tep nature and composition\" (e.g. non-determinism and labels). Finally, we develop the notion of general saturation for lax functors and show how equivalences of interest for timed behaviours are instances of this notion. This characterisation allows us to reason about the expressiveness of said notions within a uniform framework and organise them in a spectrum independent from the behavioural aspects encoded in the base category.
@inproceedings{BP16,
  author = {Brengos, Tomasz and Peressotti, Marco},
  editor = {Desharnais, Jos{\'{e}}e and Jagadeesan, Radha},
  title = {A Uniform Framework for Timed Automata},
  booktitle = {27th International Conference on Concurrency Theory, {CONCUR} 2016, August 23-26, 2016, Qu{\'{e}}bec City, Canada},
  series = {LIPIcs},
  volume = {59},
  pages = {26:1--26:15},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  year = {2016},
  url = {http://dx.doi.org/10.4230/LIPIcs.CONCUR.2016.26},
  doi = {10.4230/LIPIcs.CONCUR.2016.26}
}
Brengos, T., Miculan, M. and Peressotti, M. 2015. Behavioural equivalences for coalgebras with unobservable moves. Journal of Logical and Algebraic Methods in Programming. 84, 6 (2015), 826–852. DOI:10.1016/j.jlamp.2015.09.002.
We introduce a general categorical framework for the definition of weak behavioural equivalences, building on and extending recent results in the field. This framework is based on parametrized saturation categories, i.e. categories whose hom-sets are endowed with complete orders and a suitable iteration operators; this structure allows us to provide the abstract definitions of various (weak) behavioural equivalence. We show that the Kleisli categories of many common monads are categories of this kind. This allows us to readily instantiate the abstract definitions to a wide range of existing systems (weighted LTS, Segala systems, calculi with names, etc.), recovering the corresponding notions of weak behavioural equivalences. Moreover, we can provide neatly new weak behavioural equivalences for more complex behaviours, like those definable on topological spaces, measurable spaces, etc.
@article{BMP15,
  author = {Brengos, Tomasz and Miculan, Marino and Peressotti, Marco},
  title = {Behavioural equivalences for coalgebras with unobservable moves},
  journal = {Journal of Logical and Algebraic Methods in Programming},
  volume = {84},
  number = {6},
  pages = {826--852},
  year = {2015},
  url = {http://dx.doi.org/10.1016/j.jlamp.2015.09.002},
  doi = {10.1016/j.jlamp.2015.09.002}
}

All publications

Reviewing

I am generally happy to act as an external reviewer for papers which match my research interests, provided I can see reviews and participate in the discussion after submitting my review.