-
A Debugging System for Language-Parameterized Proofs.
Charlesowityear Ly, Eswarasanthosh Kumar Mamillapalli, Matteo Cimini.
Accepted for publication at MarjanFest'25, Festschrift in celebration of Marjan Sirjani, 2025.
-
Language-parameterized Proofs for Functional Languages with Subtyping.
Seth Galasso, Matteo Cimini.
In Proceedings of the 17th International Symposium on Functional and Logic Programming (FLOPS 2024), pages 291-310, May 2024.
-
Towards the Complexity Analysis of Programming Language Proof Methods.
Matteo Cimini.
In Proceedings of the 20th International Colloquium on Theoretical Aspects of Computing (ICTAC 2023), pages 100-118, December 2023.
-
Testing Languages with a Languages-as-Databases Approach.
Matteo Cimini.
In Proceedings of the 17th International Conference on Tests and Proofs (TAP 2023), pages 108-126, July 2023.
Best Paper Award.
-
A Declarative Validator for GSOS Languages.
Matteo Cimini.
In Proceedings of the 14th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software
(PLACES 2023), pages 14-25, April 2023.
-
Lang-n-Prove: A DSL for Language Proofs.
Matteo Cimini.
In Proceedings of the 15th ACM SIGPLAN International Conference on Software Language Engineering (SLE 2022), pages 16-29, December 2022.
-
A Query Language for Language Analysis.
Matteo Cimini.
In Proceedings of the 20th International Conference on Software Engineering and Formal Methods (SEFM 2022), pages 57-73, September 2022.
-
Lang-n-Send Extended: Sending Regular Expressions to Monitors.
Matteo Cimini.
In Proceedings of the 15th Interaction and Concurrency Experience (ICE 2022), pages 69-84, June 2022.
-
Lang-n-Send: Processes That Send Languages.
Matteo Cimini.
In Proceedings of the 13th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software
(PLACES 2022), pages 46-56, April 2022.
-
A Calculus for Multi-language Operational Semantics.
Matteo Cimini.
In Proceedings of the 13th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2021), pages 25-42, October 2021.
-
Language Transformations in the Classroom.
Matteo Cimini, Benjamin Mourad.
In Proceedings of the Combined 28th International Workshop on Expressiveness in Concurrency and 18th Workshop on Structural Operational Semantics
(EXPRESS/SOS 2021), pages 43-58, August 2021.
-
Extrinsically Typed Operational Semantics for Functional Languages.
Matteo Cimini, Dale Miller, Jeremy G. Siek.
In Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering (SLE 2020), pages 108-125, November 2020.
-
A Declarative Gradualizer with Language Transformations.
Benjamin Mourad, Matteo Cimini.
In Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages (IFL 2020), pages 44-54, September 2020.
-
On the Effectiveness of Higher-Order Logic Programming in Language-Oriented Programming.
Matteo Cimini.
In Proceedings of the 15th International Symposium on Functional and Logic Programming (FLOPS 2020), pages 106-123, April 2020.
-
System Description: Lang-n-Change - A Tool for Transforming Languages.
Benjamin Mourad, Matteo Cimini.
In Proceedings of the 15th International Symposium on Functional and Logic Programming (FLOPS 2020), pages 198-214, April 2020.
-
A Calculus for Language Transformations.
Benjamin Mourad, Matteo Cimini.
In Proceedings of the 46th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2020), pages 547-555, Limassol, Cyprus, January 2020.
-
Early Experience in Teaching the Basics of Functional Language Design with a Language Type Checker.
Matteo Cimini.
In Proceedings of the 20th International Symposium on Trends in Functional Programming (TFP 2019), pages 21-37, Vancouver, Canada, June 2019.
-
Towards Gradually Typed Capabilities in the Pi-Calculus.
Matteo Cimini.
In Proceedings of the 12th Interaction and Concurrency Experience (ICE 2019), pages 61--76, Copenhagen, Denmark, June 2019.
-
Proceedings of the 30th Symposium on Implementation and Application of Functional Languages (IFL 2018).
Matteo Cimini, Jay McCarthy.
Edited volume of the proceedings of IFL 2018, Lowell, MA, USA -- September 05 - 07, 2018.
-
Languages as First-Class Citizens (Vision Paper).
Matteo Cimini.
In Proceedings of the 11th ACM SIGPLAN International Conference on Software Language Engineering (SLE 2018), pages 65-69, Boston, USA, November 2018.
-
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.
In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), pages 789-803, Paris, France, January 2017.
-
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), article n.8, pages 1-4, 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 338-350, 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:22-50, 2016.
-
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.
-
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.
-
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.
-
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.
-
A Lightweight Formalization of the Metatheory 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.
-
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.
-
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.
-
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 2012), Bath, UK, Electronic Notes in Theoretical Computer Science, 286:103-116, 2012.
-
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.
-
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.
-
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.
-
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.
-
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
-
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 2010), Ottawa, Canada, volume 265 of Electronic Notes in Theoretical Computer Science, pages 145-160. Elsevier B.V., The Netherlands, 2010.
-
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.