Skip to Main Content

UMass Lowell will resume on-campus instruction, research and campus life for Fall 2020. View the plan for more info.

Matteo Cimini


Matteo Cimini
Matteo CiminiAssistant Professor

Research Interests

Programming Languages, Formal Methods, Interactive Theorem Proving, and Concurrent Programming.

Education

  • Ph D: Computer Science, (2012), Reykjavik University - Iceland
    Dissertation/Thesis Title: Contributions to the Meta-Theory of Structural Operational Semantics.
  • MS: Computer Science, (2008), University of Bologna - Italy
    Dissertation/Thesis Title: Lambda-calculi based on sequents: abstract machines and comparison with the π-calculus.

Selected Publications

  • Zakian, T., McDonell, T., Cimini, M., Newton, R. (2018). Ghostbuster: A Tool for Simplifying and Converting GADTs. Journal of Functional Programming.
  • , M. (2018). Languages as First-Class Citizens (Vision Paper). Proceedings of the 11th ACM SIGPLAN International Conference on Software Language Engineering (SLE 2018)
  • Cimini, M., McCarthy, J. (2018). Proceedings of the 30th Symposium on Implementation and Application of Functional Languages (IFL 2018).
  • Cimini, M., Siek, J.G. (2017). Automatically Generating the Dynamic Semantics of Gradually Typed Languages.
  • Jafari, A., Khamespanah, E., Sirjani, M., Hermanns, H., Cimini, M. (2016). PTRebeca: Modeling and Analysis of Distributed and Asynchronous Systems. (128 pp. 22-50). Science of Computer Programming
  • Cimini, M., Siek, J., Sterling, T. (2016). The Semantics of ParalleX, v1.0 (TR726:). Indiana University Technical Report
  • Cimini, M., Miller, D., Siek, J. (2016). Well-Typed Languages are Sound.
  • McDonnell, T., Zakian, T., Cimini, M., Newton, R. (2016). Ghostbuster: A Tool for Simplifying and Converting GADTs. (pp. 338-350).
  • Cimini, M., Siek, J. (2016). Fractional Permissions for Race-Free Mutable References in a Dataflow Intermediate Language.
  • Cimini, M., Siek, J.G. (2016). The Gradualizer: A Methodology and Algorithm for Generating Gradual Type Systems. (pp. 443-455).
  • Chaudhuri, K., Cimini, M., Miller, D. (2015). A Lightweight Formalization of the Metatheory of Bisimulation-Up-To. Annual Symposium on Principles of Programming Languages, 157.
  • Siek, J.G., Vitousek, M.M., Cimini, M., Tobin-Hochstadt, S., Garcia, R. (2015). Monotonic References for Efficient Gradual Typing. Programming Languages & Systems 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory & Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings, 432.
  • Garcia, R., Cimini, M. (2015). Principal Type Schemes for Gradual Programs. Annual Symposium on Principles of Programming Languages, 303.
  • Siek, J.G., Vitousek, M.M., Cimini, M., Boyland, J.T. (2015). Refined criteria for gradual typing.
  • Reynisson, A.H., Sirjani, M., Aceto, L., Cimini, M., Jafari, A., Ingolfsdottir, A., Sigurdarson, S.H. (2014). Modelling and simulation of asynchronous real-time systems using Timed Rebeca. Science of Computer Programming.
  • Cimini, M., Mousavi, M., Reniers, M.A., Gabbay, M.J. (2012). Nominal SOS. Electronic Notes in Theoretical Computer Science, 286(Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII)) 103 - 116.
  • ACETO, L., Cimini, M., INGOLFSDOTTIR, A. (2012). Proving the validity of equations in GSOS languages using rule-matching bisimilarity. Mathematical Structures in Computer Science, 22(2) 291.
  • Aceto, L., Cimini, M., Ingolfsdottir, A., Mousavi, M., Reniers, M.A. (2012). Rule formats for distributivity. Theoretical Computer Science, 458 1 - 28.
  • Luca, A., Matteo, C., Anna, I., Arni Hermann, R., Steinar Hugi, S., Marjan, S. (2011). Modelling and Simulation of Asynchronous Real-Time Systems using Timed Rebeca. Electronic Proceedings in Theoretical Computer Science, Vol 58, Iss Proc. FOCLASA 2011, Pp 1-19 (2011), (Proc. FOCLASA 2011) 1.
  • Aceto, L., Cimini, M., Ingolfsdottir, A., Mousavi, M., Reniers, M.A. (2011). SOS rule formats for zero and unit elements. Theoretical Computer Science, 412(Festschrift in Honour of Jan Bergstra) 3045 - 3071.
  • Cimini, M., Coen, C.S., Sangiorgi, D. (2010). Functions as Processes: Termination and the $$ -Calculus. Trustworthly Global Computing, 73.
  • Aceto, L., Cimini, M., Ingolfsdottir, A., Mousavi, M.R., Reniers, M.A. (2010). On Rule Formats for Zero and Unit Elements. Electronic Notes in Theoretical Computer Science, 265(Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2010)) 145 - 160.
  • Luca, A., Matteo, C., Anna, I. (2009). A Bisimulation-based Method for Proving the Validity of Equations in GSOS Languages. Electronic Proceedings in Theoretical Computer Science, Vol 18, Iss Proc. SOS 2009, Pp 1-16 (2010), (Proc. SOS 2009) 1.