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.