Matteo Cimini's publications



Drafts


  1. Well-Typed Languages are Sound.
    Matteo Cimini, Dale Miller, Jeremy G. Siek. (November 2016).
    Archived at arXiv.org.
  2. The Semantics of ParalleX, v1.0.
    Matteo Cimini, Jeremy G. Siek, and Thomas Sterling. (May 2016).
    Indiana University Technical Report TR726.
  3. Nominal Structural Operational Semantics.
    Luca Aceto, Matteo Cimini, Anna Ingólfsdóttir, MohammadReza Mousavi, Michel A. Reniers and Murdoch J. Gabbay.
    Up-to-date 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.

Publications


  1. 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.
  2. Fractional Permissions for Race-Free 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.
  3. 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 338-350, 2016.
  4. 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:22-50, 2016.
  5. The Gradualizer: A Methodology and Algorithm for Generating Gradual Type Systems.
    Matteo Cimini and Jeremy Siek.
    In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), pages 443-455, 2016.
    The Gradualizer is available online, and also at my github.
  6. 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 274--293, 2015.
  7. Monotonic References for Efficient Gradual Typing.
    Jeremy Siek, Michael M. Vitousek, Matteo Cimini, Sam Tobin-Hochstadt, and Ronald Garcia.
    In Proceedings of the 24th European Symposium on Programming (ESOP 2015), pages 432--456, 2015.
  8. Principal Type Schemes for Gradual Programs.
    Ronald Garcia and Matteo Cimini.
    In Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015), pages 303--315, 2015.
  9. A Lightweight Formalization of the Meta-theory of Bisimulation-up-to.
    Kaustuv Chaudhuri, Matteo Cimini, and Dale Miller.
    In Proceedings of the 4-th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP 2015), pages 157--166, 2015.
  10. Modelling and Simulation of Asynchronous Real-Time 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:41-68, 2014.
  11. 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:1-28, 2012.
  12. 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:103-116, 2012.
  13. Proving the validity of equations in GSOS languages using rule-matching bisimilarity.
    Luca Aceto, Matteo Cimini, and Anna Ingólfsdóttir.
    In the journal Mathematical Structures in Computer Science, 22(2):291--331, Cambridge University Press, 2012.
  14. Modelling and simulation of asynchronous real-time 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 1-19, 2011.
  15. 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 79-90, Springer-Verlag, 2011.
  16. 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):3045-3071, 2011.
  17. Functions as processes: Termination and the Lambda-bar-mu-mu-tilde-Calculus.
    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 73-86, Springer-Verlag, 2010. Online Appendix
  18. 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 145-160. Elsevier B.V., The Netherlands, 2010.
  19. A bisimulation-based 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 1-16, 2010.

Ph.D. Thesis, and M.Sc. Thesis


  1. Contributions to the Meta-Theory of Structural Operational Semantics.
    Ph.D. Thesis. Matteo Cimini. Reykjavik University, 2012.
  2. Lambda-calculi based on sequents: abstract machines and comparison with the pi-calculus.
    M.Sc. Thesis. Matteo Cimini. University of Bologna, 2008.
    Supervised by Davide Sangiorgi and Claudio Sacerdoti Coen.