Dipartimento di Informatica

MeCTAFI:

Constructive Methods in Topology, Algebra and Foundations of Computer Science
(Metodi Costruttivi in Topologia, Algebra e Fondamenti dell'Informatica)

MIUR-PRIN bando 2008

The goal of the project is the comparison between constructive and predicative mathematics with classical and impredicative mathematics. The concepts used to bridge the gap between the two approaches are from topology, category theory, and learning in the limit.  We use a constructive version of the definition of limit in order to describe the notion of learning, and category theory in order to describe
the model we obtain. We aim to show how learning in the limit provides a constructive interpretation of classical logic.

The project will concentrate on the computational aspects of constructive mathematics. We ask ourselves whether programs extracted from classical proofs should be represented by plain lambda terms, or by adding new operators representing continuations, state updating, non-deterministic choice, parallel composition and so on.


URL: http://prin.miur.it/