scrap

It is difficult to resume 30+ years of research in a single page. But if I had to resume in few words, I would say this:

I like machines in general, and computer in particular, because they are stupid and simple, compared to the complexity of other subjects (especially humans). Biological systems are the result of a random-based selection-driven evolution. They are not the result of a (semi)rational, planned design. Understanding their behaviour is a mess. Instead, systems and computers are designed by humans. And this is an advantage we must be aware of. Because if we design them, we are in the position to understand, control and determine their behavior. The converse is not true. Never will be.

From this point, my research follows.

It is difficult to summarise over three decades of research, but I can say that my research has consistently focused on developing and applying formal methods to model and understand complex systems, in order to enhance their trustworthiness. Along all these years, my interests have evolved within this broad landscape, tackling new challenges as they emerged. I will recall here some achievements.

My initial work (1994-1997 and 2000-2006) centered on formalizing programs and processes within logical frameworks and proof assistants built on type theory (e.g., Lego, Coq). Recognizing the theoretical and practical limitations of existing tools, I concentrated on developing novel techniques to streamline the formalization and reasoning process. A key outcome of this effort was the introduction of the weak Higher-Order Abstract Syntax (weak HOAS) technique for handling binders in inductive type theories (Honsell & Miculan, 1995)(Miculan, 1997)(Miculan, 1999). This innovation, now a standard techniques within the Coq community, continues to be actively used for reasoning about languages with binders.
While powerful, weak HOAS presents challenges for reasoning by induction over higher-order terms. To address this, we introduced the Theory of Contexts, a set of three axioms that demonstrably improve inductive reasoning (Honsell et al., 2001); this work is still a landmark in formal reasoning about π-calculus and similar models in Coq. However, adding axioms to a complex system like Coq requires careful consideration. We formally proved the soundness of the Theory of Contexts using category-theoretic constructions called tripos (Bucalo et al., 2006). This work, in collaboration with the late Martin Hofmann, marked my second significant encounter with category theory, which became a cornerstone of my subsequent research.
As a side note, the introduction of (weak) HOAS sparked significant interest in the research community around higher-order abstract syntax and binders, yielding three influential papers at LICS 1999 (Fiore et al., 1999; Hofmann, 1999; Gabbay and Pitts, 1999). In particular, the latter laid the foundation for the new and thriving area of theoretical computer science called “nominal techniques”. We have investigated the connections between these approaches to binders in (Miculan & Yemane, 2005)(Gadducci et al., 2006).

Another limitation of type theory-based logical frameworks is that circular definitions are subject to syntactic restrictions to ensure their termination and productivity. These restrictions decrease the expressive power of the language. To address this problem, we have proposed a very general Banach-like theorem for defining fixed-points in categories of sheaves (Di Gianantonio & Miculan, 2004). This result gives a unifying and general account of most techniques used in computer science in order to ensure convergency of circular definitions, such as well-founded recursion and contractivity in complete ultrametric spaces. Furthermore, to achieve a more natural and practical approach, we introduced the notion of complete ordered families of equivalence relations (COFE) in (Di Gianantonio & Miculan, 2003). COFE offer a more intuitive alternative to specific ultrametric spaces and integrates well with formalizations. This led to COFE becoming a standard tool in synthetic guarded domain theory and step-indexed logical relations like in Iris, a verification framework crucial for proving the correctness and semantic soundness of the Rust programming language. This interesting subject re-emerged during a visit to Aarhus years later, resulting in a collaborative work with Lars Birkedal’s group (Bizjak et al., 2014).

My exploration of logical frameworks sparked an interest in metamodels, which became a main subject of my second research period (2006-2015). Metamodels are abstract frameworks that allow for proving general results about entire classes of models. Logical frameworks themselves can be viewed as logical metamodels, ideal for reasoning about logical systems. Other metamodels offer advantages for reasoning about the operational semantics of programs and processes. I particularly delved into Bigraphs and Bigraphical Reactive Systems (BRSs), a graphical metamodel conceived by Robin Milner. BRSs offer a powerful approach to describing the syntax and semantics of distributed systems by leveraging the distinct concepts of connectivity and locality. To address limitations in original bigraphs, we introduced directed bigraphs (Grohmann & Miculan, 2007). This extension enhanced expressivity while preserving the core strengths of bigraphs, particularly the RPO construction and bisimulations. Directed bigraphs proved valuable for modeling various systems, including Fusion calculus (previously incompatible with standard bigraphs) (Grohmann & Miculan, 2007), Access control systems (Grohmann & Miculan, 2008), Systems biology (Bacci et al., 2009)(Bacci et al., 2009), Multi-agent systems (Mansutti et al., 2014). Furthermore, I actively contributed to bigraph tooling. Our initial DBtk toolkit (Bacci et al., 2009) has been succeeded by jLibBig, a Java library for bigraphs and BRSs, which remains actively developed and used by the community.

My work on modelling Fusion calculus with bigraphs led me to investigate bialgebras, a unifying framework for operational and denotational semantics introduced by Turi and Plotkin. In earlier work (Miculan & Scagnetto, 2003), I had already extended this framework to typed higher-order abstract syntax and semantics. Inspired by applications in systems biology (Bacci & Miculan, 2010)(Bacci & Miculan, 2012), I became interested in using bialgebras and related GSOS rule formats to model quantitative aspects of systems. This resulted in the introduction of the first structural operational semantics for continuous state probabilistic processes (Bacci & Miculan, 2012) and a general GSOS for non-deterministic processes with quantitative features (Miculan & Peressotti, 2014). We further developed a generic algorithm for deciding weak bisimulations over a broad class of weighted labeled transition systems (Miculan & Peressotti, 2017). Finally, in (Bernardo & Miculan, 2016)(Bernardo & Miculan, 2019), we established a surprising result: disjunctive probabilistic modal logic can fully characterize bisimilarity on reactive probabilistic systems (also known as Markov decision processes).

…to be continued…

distributed systems, protocol, security