### 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.)