My research, in brief. My research is in proof theory and its applications to non-classical logics: modal, intuitionistic, substructural, temporal, many-valued and ecumenical logics, together with geometric logic. A guiding theme is a unified proof theory. For a given logic, I look for sequent calculi in which all structural rules are admissible (labelled, G3-style and G0-style), natural deduction with general elimination rules, and axiomatic systems. These are linked by bidirectional translations that yield cut elimination, full normalization, countermodel extraction and, in the terminating cases, decidability. 

Rationale: The early years of modal logic saw the characterisation of its basic notions in terms of the axiomatic method. Later, with the invention of Hintikka-Kripke's semantics, semantical methods became the dominant approach of philosophers, mathematicians, and computer scientists. These methods, however, do not reflect the structure of the inferential processes that are necessarily connected to a logical representation.

Here modern proof theory comes to rescue; in fact, it was born out of dissatisfaction with the axiomatic logical method in view of a faithful presentation of the processes of logical inference.

My early work in this area, from 1997 to 2003, has been mainly in pure proof theory, in the tradition of Gentzen, Ketonen, Dragalin and Troelstra. In 2003, I found a way of extending the results for pure predicate logic to logics that can be characterized in terms of Kripke semantics. With this in hand, I had a clue to develop inferential systems for modal logic, which at that time was considered impossible by many.

A decisive step in the programme I carried out subsequently was the formulation of systems of basic modal logic as systems of rules of proof within a well-developed methodology for the analysis of the structure of proofs. The seminal paper in the topic appeared in 2005 and has become a widely cited and very influential work and the basis of several doctoral theses, both in Finland and abroad; an exposition forms the fourth part of my monograph "Proof Analysis" with Jan von Plato.

More recently, I have extended this line of research in scope and methodology. A more fine-grained topological semantics now covers counterfactual reasoning, non-normal modalities, doxastic notions and epistemic dynamics. With Norihiro Kamide, I have developed unified sequent calculi and natural deduction systems with full normalization for logics of strong negation, extended Belnap–Dunn and intuitionistic logics (including Nelson and Gurevich logics), until-free linear-time temporal logics, and intermediate logics. The most recent work in this series introduces a new ecumenical logic that combines intuitionistic and classical reasoning in a single language through one synthesizing operator ♯. It comes with a simulation theorem into classical logic, decidability via an embedding, cut elimination, and a Hilbert-style system. With Matteo Tesi I have studied infinitary intuitionistic logic and the conversion of axioms into rules in intuitionistic logic. With Giulio Fellin and Eugenio Orlandelli the topics are constructive cut elimination for geometric logic and terminating intuitionistic calculi, and with Cosimo Perini Brogi and Nicola Olivetti modular calculi for interpretability logics. A historical strand, with Jan von Plato, concerns Gödel’s early work on intuitionistic and modal logic and the edition of Oiva Ketonen’s thesis.

Short bio. I am professor (it.: Professore Ordinario) of Mathematical Logic at the University of Genova. During 2015-2019 I have held the chair of Theoretical Philosophy at the Philosophy Unit of the Department of Philosophy, History and Culture of the University of Helsinki. Previously I have been a Researcher/Senior Researcher since 1996 and Logiikan Dosentti (Adjunct Professor in Logic) since 1998 in the same department (a title resumed in 2021), and research fellow at the Helsinki Collegium for Advanced Studies from 2014 to 2015. I obtained a Master degree in Mathematics in 1991 and a Ph.D. in Mathematics in 1996, both at the University of Padova. I visited various universities (Amsterdam, Chalmers, St Andrews, Toulouse), have been a research associate at the Department of Computing of the Imperial College in London, a Humboldt Fellow at the Department of Mathematics of LMU in Munich, and a visiting scientist at the Mittag-Leffler mathematical research institute in Stockholm and at the Hausdorff Research Institute for Mathematics in Bonn. I have held a number of specialised courses in Summer Schools and invited lecture series to students from mathematics, philosophy and computer science. I have consolidated experience of reserch group leadership and have supervised five doctoral dissertations. During 2013-2014 I have obtained the National Scientific Qualification to associate and full professorship in Italian Universities for the academic fields of ''Logica Matematica e Matematiche Complementari (01/A1)'' and ''Logica, Storia e Filosofia della Scienza (11/C2)'', and to associate professorship in ''Informatica (01/B1)''.

CV (pdf).

Projects:

   MOSAIC: Modalities in Substructural Logics: Theory, Methods and Applications (2021-2025) H2020

Infinity and Intensionality: Towards A New Synthesis, (2021 – 2024) Research Council of Norway

Academy of Finland project (2017-2021): Modalities and conditionals: Systematic and historical studies

Former representative for Finland for the European research network on types for programming and verification (EUTYPES) COST action

• Activity and publications:

  • My Google Scholar Page

  • Research database TUHAT

  • List of main publications

  • Publications by subject (updated up to 2018)

  • A reasoned bibliography 1998-2002

• Recent and forthcoming events:

• IJCAR 2026 International Joint Conference on Automated Reasoning (Lisbona, July 26-29, 2026)

• Taming the Infinite: Logic, Algebra, and Constructive Mathematics (Verona, April 20, 2026)

• Proof, Argumentation, Computation, Modalities And Negation (PACM∧N) (Verona, June 10–12, 2026)

• Proof Systems in Actual Practice: Reasoning and Computation (Dagstuhl, March 15-20, 2026)

• 4th ECUMENICAL meeting (Stockholm University, February 18-20, 2026)

• Synthetic mathematics, logic-affine computation and efficient proof systems (Luminy, September 8–12, 2025)

• Realism and anti-realism. Paradigms and research programmes in logic and the philosophy of mathematics (Carl Friedrich von Weizsäcker-Center, University of Tübingen , April 28-29, 2025)

• Autumn school "Proof and Computation",  (Fischbachau, September 15-21,2024)

• Proof Representations: From Theory to Applications, (Dagstuhl Schloss, August 18-24, 2024)

•  Proof Theory and Theoretical Computer Science Special session of the 2nd AMS-UMI International Joint Meeting (Palermo, July 23-24, 2024)

• Scandinavian Logic Symposium (Reykjavik, June 10-13, 2024)

• From Proofs to Computation in Geometric Logic and Generalizations (Dagstuhl Schloss, January   7–12, 2024)

• CLAR 2023 (5th International Conference on Logic and Argumentation, Hangzhou, 10-12 September)

• Congresso UMI 2023 (Pisa 4-9 September 2023)

• CLMPST 2023 (Buenos Aires, 24-29 July)

• Type Theory, Constructive Mathematics and Geometric Logic (Luminy, 1-5 May 2023)

• Past events

• Teaching (past)