ACTIVITIES

Constructivism - which arose hystorically as an alternative to classical mathematics which suffered from the paradoxes at the beginning of the 20th century - in the past few years has acquired radically new motivations and applications, coming directly from the research practice. This new way of understanding constructivism has emerged in seemingly different fields.

In logic, type theories, originated with Russell and others, found a precise and constructively convincing formulation by P. Martin-Löf in the early 70's. In that formulation, truth is meant as provability, and infinity is a construction process. Furthermore, quantification makes sense only on types obtained by a generation process. In category theory, the important constructions are given by means of coherence structures which control the data algebraically. Examples are everywhere: in algebraic topology, in algebraic geometry, in logic, in theoretical computer science. Such constructions are often determined by universal properties. In information technology, constructive type theory has been developed in the introduction of the so-called functional programming languages, and in the analysis of the properties of programs such as correctness of the code with respect to a given specification, termination, and reachability. Researchers at DISI have obtained crucial results about models of functional languages using the specific universal constructions of categories: completions by quotients.

At present, we are mainly concerned with the study of the connections between completion by quotients of categories and predicative type theory. We hope to use these to produce a fresh, elementary approach to topology, and, at the same time, to offer a common ground for many different kinds of mathematical modelling. We are also try to obtain a direct connection between constructive type theory and universal constructions, since all these have an extemely explicit, finitary presentation.

(Collaboration with Università dell'Insubria, Università di Padova, Queen Mary and Westfield, London, University of Edinburgh.)