My research is mostly about semantic metamodels (called also frameworks), that is, general mathematical theories for developing and studying models of programs and processes.
As other formal methods, these models are useful for understanding (analyze), specifying, developing and verifying formally program and processes. Also, the design and implementation of any modern programming language is always backed up by a clear semantic model. But developing appropriate models is not easy. Thus, we may consider framework theories which provide general, structural results which prevent us from duplicating efforts in developing the models of specific systems and languages. These framework theories are the “computational metamodels” that I work about. Many framework theories have been and still are studied and developed; there are frameworks for operational semantics (such as GSOS, graph rewriting systems, Milner’s bigraphs), for denotational semantics (such as algebraic/coalgebraic/bialgebraic specifications, monads, enriched Lawvere theories, mathematical operational semantics), and for logical semantics (such as metalanguages for deductive systems, i.e. Logical Frameworks). However, the boundaries among these areas are somehow blurred, and often techniques and ideas from one can be reapplied in the others. In fact, I work in all of them, using techniques from mathematical logic, type theory and category theory.
But theoria must be accompanied by poiesis and praxis. Thus I am also interested in applications of these (meta)models, both in conventional fields (such as local and distributed computing, networks, security, etc) and in new, emerging areas. An excellent example of the latter is the new, exciting field of systems biology (not to be confused with bioinformatics).
Look also at my publications.
Recent research projects
- Reduction Systems: synthesis, refinement and verification of behavioural models (SisteR) (MiUR PRIN 20088HXMYN)
- Analysis of Reaction systems with Transitions systems (ART) (MiUR PRIN 2005015824)
- Types for Proofs and Programs (TYPES) (EU FP6 IST-CA-510996)
Older projects include “Levi” (40% 1997), TOSCA (COFIN99), TYPES (EU ESPRIT BRA 6453), TYPES (ESPRIT WG 21900), TYPES (IST WG 29001), Computational Metamodels (COMETA) (MIUR COFIN 2001), Dynamic Assembly, Reconfiguration and Type-checking (DART) (EU IST-2001-33477).
Conferences and workshops committees
- 2013: CALCO’13 (PC member), TYPES’13 (PC member)
- 2011: FOSSACS’11 (PC member)
- 2010: Logical Frameworks and Meta-Languages: Theory and Practice (PC Co-chair, Steering committee member)
- 2009: Logical Frameworks and Meta-Languages: Theory and Practice (PC member), Membrane Computing and Biologically Inspired Process Calculi (PC member).
- 2008: Mathematically Structured Functional Programming (PC member).
- 2007: Logical Frameworks and Meta-Languages: Theory and Practice (PC member); TYPES 2007 (OC and PC member), Effects and Type Theory, EffTT.
- 2006: Mathematically Structured Functional Programming (PC member); IFIP WG 2.2 Anniversary Meeting (OC member).
- 2005: ACM SIGPLAN MERλIN’05 (PC member); AICA 2005 (PC member).
- 2003: ACM SIGPLAN MERλIN’03 (PC member, OC member); COMETA 2003 final workshop (OC member).
- 2002: COMETA kickoff meeting (OC member), and GioCoNOpLe (OC member).
- 2001: TOSCA’01 Final workshop (OC member)