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.

Developing appropriate models is not easy; thus, we can 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 *meta*models” 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, such as the new field of systems biology (not to be confused with bioinformatics).

Look also at my publications.