Type Theory. In particular, theories of types underpinning Logical Frameworks are studied, these being highly typed programming languages combining two computational modes that are reciprocally dual: reduction and pattern-matching. They also are, as a matter of fact, foundational theories in constructive logic, which were recently the object of great attention also within the scope of Geometric Algebra, giving rise to the Homotopy Type Theory. This thread is closely related with research themes concerning the area of Languages and Formal Methods.

Foundations of Computational and Process Semantics. In Semantics, there is a duality between processes and computation, between evolutionary systems (behavioural semantics) and reduction systems (reduction semantics) that has not been entirely clarified yet. The goal is compositionality, in order to allow for references to be transparent. On the one hand, there is the denotational, initial, bottom-up semantics to be analysed by means of induction principles, on the other hand there is the operational, final, top-down semantics, to be analysed by means of co-induction principles. The latter semantics is linked with hypersets, and with the bisimulations that were introduced independently in various sectors of logic in the early 1980s and by Forti and Honsell in the Set Theory in 1982. Starting again from these original concepts, the Set Theory of Fitch was recently studied and implemented within the LLFP; this is a theory that is very close to the ideal theory of Cantor. Although paraconsistent, it is not banal, because it only allows demonstrations in normal form. It is, however, particularly suitable for verifying programs because it is very expressive, since it allows us to reason freely thanks to the Comprehension Principle, and to postpone the verification of normalisation to when it is really necessary. Also, suitable quotients of the term models of Fitch's Theory provide interesting hyperuniverses, for instance a further definition of finitary hypersets. Typical tools of denotational semantics, Scott's domains, are used in order to describe constructional analysis. In particular, we deal with the problem of constructionally defining the differential operator, by choosing suitable representations for real numbers and for the functions upon these.

Game Semantics and Games for the Sematics of Programming and Interaction Languages. During the 1990s, J.-Y. Girard introduced the Geometry of Interaction, allowing a revolutionary way of studying the duality between operational semantics and denotational semantics, because it introduces a conceptually new intermediate space between these two. The Geometry of Interaction gave rise to the game semantics, that allowed the designing of fully abstract models for functional programming languages, with different sorts of primitives, including non-functional ones. By means of the concept of gaming, as an alternation of interactions, unexpected links of the computational theory emerged, connecting it with several branches of logic and theoretical physics. Abramsky and Lenisa studied, during the early 2000s, a model of Geometry of Interaction that was proven to be particularly suitable for discussing reversible computation. The most recent specific objective is that of studying the properties of pattern-matching automata that provide a model of Linear Combinatory Logic. In particular, a lambda calculation was introduced, extended to a discipline of types having a non-symmetrical intersection, whose main types directly allow for the derivation of the semantics of the Geometry of Interaction for linear combinatory logic. This is a very promising approach and it might offer the key to the understanding of the deep nature of this intermediate realm, that is compositional but also operational, called Geometry of Interaction.