Towards an Implementation in Lambda-Prolog of Maietti's two-level minimalist foundation.

The idea of a theory able to conjugate the advantages of both the extensional and intensional views of mathematics was presented in an article by Maria Emilia Maietti in 2006. In order to combine these two different views the theory is developed over two levels: an extensional level interpreted over an intensional one by means of quotients. The first attempt to fully formalize this theory in a programming language is the subject of Alberto Fiori's master thesis. After giving a brief introduction to Maietti's theory in the first two chapters, I proceed to examine Fiori's implementation in Lambda-Prolog, focusing on its main downside: in the translation from extensional types to their intensional interpretation, the size of the translated types grows exponentially. Such an explosive growth renders Fiori's approach computationally unviable. In order to deal with this issue we had to devise a different approach, an implementation (written in the same language) which effectively builds the setoid model in the intensional theory and then uses this new level of abstraction to implement the extensional theory. In practice, this means building a library of abstractions where the definitions of setoid and dependent setoid are given once and for all. This required us to write our own abstraction mechanisms for abstracting over types, terms and conversion rules, since Maietti's theory does not provide a definitional level. The new abstraction mechanisms presented in this thesis represent therefore an original contribution to Maietti's work. Finally, I show that while the size of translations is smaller in this implementation, its growth remains exponential. Thanks to the setoid approach, however, the reasons behind the explosive size growth have finally become more clear: this makes them easier to analyse and, hopefully, will allow future implementations to overcome this issue.