
WellTyped Languages are Sound.
Matteo Cimini, Dale Miller, Jeremy G. Siek. (November 2016).
Archived at arXiv.org.
Slides of a related presentation at SNAPL 2017. (invited junior researcher presentations).

The Semantics of ParalleX, v1.0.
Matteo Cimini, Jeremy G. Siek, and Thomas Sterling. (May 2016).
Indiana University Technical Report TR726.

Nominal Structural Operational Semantics.
Luca Aceto, Matteo Cimini, Anna Ingólfsdóttir, MohammadReza Mousavi, Michel A. Reniers and Murdoch J. Gabbay.
Uptodate online resource (2015). See the related project website.
Expanded description of the Nominal SOS framework. This draft is based on Chapter 5 of my Ph.D. thesis and will be finalized for a journal submission.

Ghostbuster: A Tool for Simplifying and Converting GADTs.
Timothy Zakian, Trevor McDonell, Matteo Cimini, Ryan Newton.
In the journal Journal of Functional Programming (JFP), Volume 28, e16, 2018.

Automatically Generating the Dynamic Semantics of Gradually Typed Languages.
Matteo Cimini and Jeremy Siek.
To appear in Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), Paris, France, January 2017.

Fractional Permissions for RaceFree Mutable References in a Dataflow Intermediate Language.
Matteo Cimini and Jeremy Siek.
In Proceedings of the 1st Workshop on Programming Models and Languages for Distributed Computing (PMLDC 2016) , Rome, Italy, July 2016.

Ghostbuster: A Tool for Simplifying and Converting GADTs.
Trevor McDonell, Timothy Zakian, Matteo Cimini, Ryan Newton.
In Proceedings of the 21st annual ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), pages 338350, 2016.

PTRebeca: Modeling and Analysis of Distributed and Asynchronous
Systems.
Ali Jafari, Ehsan Khamespanah, Marjan Sirjani, Holger Hermanns, Matteo Cimini.
In the journal Science of Computer
Programming, 128:2250, 2016.

The Gradualizer: A Methodology and Algorithm for Generating Gradual Type Systems.
Matteo Cimini and Jeremy Siek.
In Proceedings of the 43rd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL 2016), pages 443455, 2016.
The Gradualizer is available online, and also at my github.

Refined Criteria for Gradual Typing.
Jeremy Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland.
In Proceedings of The Inaugural Summit oN Advances in Programming Languages (SNAPL 2015), pages 274293, 2015.

Monotonic References for Efficient Gradual Typing.
Jeremy Siek, Michael M. Vitousek, Matteo Cimini, Sam TobinHochstadt, and Ronald Garcia.
In Proceedings of the 24th European Symposium on Programming (ESOP 2015), pages 432456, 2015.

Principal Type Schemes for Gradual Programs.
Ronald Garcia and Matteo Cimini.
In Proceedings of the 42nd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL 2015), pages 303315, 2015.

A Lightweight Formalization of the Metatheory of Bisimulationupto.
Kaustuv Chaudhuri, Matteo Cimini, and Dale Miller.
In Proceedings of the 4th ACMSIGPLAN Conference on Certified Programs and Proofs (CPP 2015), pages 157166, 2015.

Modelling and Simulation of Asynchronous RealTime Systems using Timed Rebeca.
Arni Hermann Reynisson, Marjan Sirjani, Luca Aceto, Matteo Cimini, Ali Jafari, Anna Ingólfsdóttir and Steinar Hugi Sigurdarson.
In the journal Science of Computer Programming, 89:4168, 2014.

Rule formats for distributivity.
Luca Aceto, Matteo Cimini, Anna Ingólfsdóttir, Mohammadreza Mousavi, and Michel A. Reniers.
In the journal Theoretical Computer Science, 458:128, 2012.

Nominal SOS.
Matteo Cimini, MohamamdReza Mousavi, Michel A. Reniers and Murdoch J. Gabbay.
In Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII), Bath, UK, Electronic Notes in Theoretical Computer Science, 286:103116, 2012.

Proving the validity of equations in GSOS languages using rulematching bisimilarity.
Luca Aceto, Matteo Cimini, and Anna Ingólfsdóttir.
In the journal Mathematical Structures in Computer Science, 22(2):291331, Cambridge University Press, 2012.

Modelling and simulation of asynchronous realtime systems using Timed Rebeca.
Luca Aceto, Matteo Cimini, Anna Ingólfsdóttir, Arni Hermann Reynisson, Steinar Hugi Sigurdarson, and Marjan Sirjani.
In Proceedings of the 10th International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA 2011), volume 58 of Electronic Proceedings in Theoretical Computer Science, pages 119, 2011.

Rule formats for distributivity.
Luca Aceto, Matteo Cimini, Anna Ingólfsdóttir, Mohammadreza Mousavi, and Michel A. Reniers.
In Proceedings of the 5th International Conference on Language and Automata Theory and Applications (LATA 2011), volume 6638 of Lecture Notes in Computer Science, pages 7990, SpringerVerlag, 2011.

SOS rule formats for zero and unit elements.
Luca Aceto, Matteo Cimini, Anna Ingólfsdóttir, MohammadReza Mousavi, and Michel A. Reniers.
In the journal Theoretical Computer Science, 412(28):30453071, 2011.

Functions as processes: Termination and the LambdabarmumutildeCalculus.
Matteo Cimini, Claudio Sacerdoti Coen, and Davide Sangiorgi.
In Proceedings of the 5th Symposium on Trustworthy Global Computing (TGC 2010), volume 6084 of Lecture Notes in Computer Science, pages 7386, SpringerVerlag, 2010. Online Appendix

On rule formats for zero and unit elements.
Luca Aceto, Matteo Cimini, Anna Ingólfsdóttir, MohammadReza Mousavi, and Michel A. Reniers.
In Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVI), Ottawa, Canada, volume 265 of Electronic Notes in Theoretical Computer Science, pages 145160. Elsevier B.V., The Netherlands, 2010.

A bisimulationbased method for proving the validity of equations in GSOS languages.
Luca Aceto, Matteo Cimini, and Anna Ingólfsdóttir.
In Proceedings of the 6th Workshop on Structural Operational Semantics 2009 (SOS 2009), August 31, 2009, Bologna (Italy), volume 18 of Electronic Proceedings in Theoretical Computer Science, pages 116, 2010.

Contributions
to the MetaTheory of Structural Operational Semantics.
Ph.D. Thesis. Matteo Cimini. Reykjavik University, 2012.
Advisors: Luca Aceto and Anna Ingólfsdóttir.

Lambdacalculi based on sequents: abstract machines and comparison with the picalculus.
M.Sc. Thesis. Matteo Cimini. University of Bologna, 2008.
Supervised by Davide Sangiorgi and Claudio Sacerdoti Coen.