icona researchResearch

Settore scientifico disciplinare di attività: INF_01 - INFORMATICA

My research interests have focused on mathematical structures for the semantics of programming languages, and on semantical aspects of type systems, especially those that include recursive types. I also studied the conceptual aspects and the historical development of type theories and lambda-calculus. In more detail, I have recently been concerned with the following themes:

Properties of infinite objects
Several functional programming languages, notably Haskell, allow circular definitions of ÒinfiniteÓ data structures like, e.g., the streams:
ones = 1 : ones nats = from(0) where from(n) = n : from(n+1)

The types of such data structures are circular as well, for example ones has type [Integer], where [Integer], the type of finite lists and streams of integers, is recursively defined by the equation:
[Integer] = [] | Integer : [Integer].

In order to prove properties of these circular definitions and of the objects they define, it is common to use coinduction and the fact that such objects are elements of final coalgebras. I have been investigating alternative techniques related to the Approximation Lemma to prove properties of streams and other infinite objects, exploiting the sheaf-like structure that arises from an explicit stratification of infinite objects into tiers.

Recursive types
I started my research on recursive types in 1986; most of it has been carried out in collaboration with Mario Coppo, of the University of Torino. I investigated the application of coalgebraic techniques to recursive types. I also studied the global structure of recursive types as an iterative algebraic theory (the latter is a by now fairly standard approach to cyclic structures invented by Elgot in the late '60s). A comprehensive treatment of several approaches to the syntax and semantics of recursive types, written with Mario Coppo, appeared in 2012 for Cambridge University Press in a volume edited by Barendregt, Dekkers and Statman.

Foundational and philosophical aspects of computer science: I also have a strong interest for foundations and philosophical issues in informatics as a science (as opposed to engineering). Among such issues, along the years I pursued the following, with varying degrees of involvement:

  • the foundations of classical computability theory, especially the Church-Turing Thesis from an epistemological point of view
  • the foundations of complexity theory Ð in particular the identification of polytime with feasible computation (the so called Edmonds-Cobham-Cook-Karp thesis) and the relations of this with ultrafinitism as a philosophy of mathematics
  • the abstract theory of computation that arises from the theory of domains, especially the domains associated with event structures
  • the theory of computation that arises from the ideas of Carl Adam Petri and Anatol W. Holt
  • the historical and conceptual development of lambda-calculus and combinatory logic, especially in connection with the applications of these in theoretical computer science

My research groups: