The group operates within the scope of Informatic Formal Methods and deals with the following research themes.

Logical Frameworks and Interactive Environments for Formalised Reasoning. The goal of this research area is developing the theory and experimenting with the implementation of interactive environments (editors) that can assist the users of logic-formal methods for the certification and development of software. The Logical Frameworks taken into account are all based on the Constructive Type Theory, therefore on the analogies of formulas-as-types and of judgments-as-demonstrations, developed by Martin-Lof and by Plotkin-Harper-Honsell in the 1980s. Their LF theory was the first metalanguage for formal derivations that was directly implementable, that is why it was granted the IEEE Logic in Computer Science Test-of-Time Award in 2007. Over the last 30 years, the field grew a lot, and the research group of Udine published over 50 works, always being a leading member in the European TYPES network. The most recent research objective of the group is implementing LLFP, a Logical Framework that allows fast prototyping, but in an absolutely transparent way, by using the monad mechanism, specific editors for complex programming logics. That is, when the logics make use of non-formal external evidence coming from heterogeneous sources or feature arbitrary constraints (side conditions) about the form of derivations. A first prototype of the LLFP type checker was recently implemented in OCaml by Vincent Michielini of the ENS of Lyon, within the framework of a research stage with the scientific collaboration of Luigi Liquori of the INRIA of Sophia Antipolis, too.

The group is also committed to adapting the synthesis capabilities of logical frameworks based on the type theory to new computational aspects. In particular, by exploiting the Curry-Howard isomorphism, a methodology was developed in order to synthesise certified, distributed Erlang programs, starting from demonstrations in Coq. Finally, appropriate logical frameworks (e.g. rewriting logic) were used for developing new verification and formal analysis methodologies for concurrent systems.

Set and Category Models of Infinite Objects. The goal of this research area is studying both set and category models in order to capture the behaviour of infinite processes.