A. Bossi, S. Valentini, La teoria Intuizionistica dei tipi: una introduzione e il teorema di normalizzazione,

in "I convegno nazionale sulla programmazione logica GULP", Genova, 1986.

Abstract: Il lavoro presenta una prima introduzione alla teoria dei tipi di Martin-Löf sia dal punto di vista sintattico che semantico e mostra le idee che stanno alla base della prova della normalizzabilità delle sue prove.

A. Bossi, S. Valentini, Assunzioni di arietà superiore nella teoria intuizionistica dei tipi,

atti del "II convegno nazionale sulla programmazione logica GULP", Torino, 1987, pp. 81-92.

Abstract: Il lavoro mostra come introdurre assunzioni di arietà superiore, vale a dire assunzioni sulla verità di una derivazione invece che della verità di una proposizione, nella teoria intuizionista dei tipi di Martin-Löf. Alcune conseguenze di questa possibilità vengono poi analizzate.

A. Bossi, S. Valentini, An intuitionistic theory of types with assumptions of high-arity variables,

Annals of Pure and Applied Logic 57, North Holland, 1992, pp.93-149.

Abstract: After some introductory observations on Martin Löf's Intuitionistic Theory of Types (ITT), the paper introduces the notion of assumption of high arity variable, which extend the original theory in a very uniform way (HITT). Some improvements to the exposition of HITT, allowed by high arity variables, are then shown. The main result of the paper follows: a normal form theorem for HITT, and hence for ITT, is proved using a computability method à la Tait. Finally its main consequences are illustrated: the consistency of HITT, which also implies the consistency of ITT, and the computability of any judgement derived within HITT. Beside we proved a canonical form theorem: to any derivable judgement we can associate a canonical one whose derivation ends with an introductory rule from which the standard disjunction and existential properties follow. Moreover, by using the computational interpretation of types it immediately follows that the execution of any proved correct program terminates.

S. Valentini, Another introduction to Martin-Löf's Intuitionistic Type Theory,

in "Trends in Theoretical Informatics", eds. R. Albrecht and H. Herre, Innsbruck, 1996.

Abstract: First an introduction to Martin-Löf's type theory is given. Then some examples of programs developed within the theory are shown and finally the main metamathematical properties of the theory are recalled.

S. Valentini, Decidability in Intuitionistic Theory of Types is functionally decidable,

Mathematical Logic Quarterly 42 (1996), pp. 300-304.

Abstract: In this paper we show that the usual intuitionistic characterization of the decidability of the propositional function is equivalent, when working within the framework of Martin-Löf's Intuitionistic Type Theory, to require that there exists a decision function. All the proofs are carried out within the Intuitionistic Type Theory and hence the decision function is effectively constructed.

D. Maguolo, S. Valentini, An intuitionistic version of Cantor's theorem,

Mathematical Logic Quarterly (1996).

Abstract: An intuitionistic version of Cantor's theorem, which shows that there is no surjective function from the set of the natural numbers N into the set of the functions from N into N, is proved within Martin-Löf's Intuitionistic Type Theory with the universe of the small sets.

G.Sambin, S.Valentini, Building up a toolbox for Martin-Löf intuitionistic type theory,

in "Twenty five years in Intuitionistic Type Theory", 1996.

Abstract: A full theory of subsets is developed completely inside Martin-Löf's type theory.

S. Valentini, The forget-restore principle: a paradigmatic example,

in "Twenty five years in Intuitionistic Type Theory", 1996.

Abstract: A proof is shown of the possibility to treat constructively with proof-irrelevance within Martin-Löf's type theory.

M. E. Maietti, S. Valentini, Can you add power-sets to Martin-Löf's intuitionistic set theory?,

Mathematical Logic Quarterly, vol. 45 (1999), pp. 521-532.

Abstract: An extension of Martin-Löf's intensional set theory is proposed by means of a power-set. Since the equality among subsets has to be extensional, such extension is not constructive, in the sense that any link between the truth of a proposition and the possibility to exhibit one of its proof-element is lost. This fact is not compatible with the usual rules of intuitionistic set theory. In fact we can prove that this extension is classic as a consequence of the intuitionistic axiom of choice.

S. Valentini, The formal development of non-trivial programas in constructive type theory,

proceedings of MPCS96, Ischia, maggio 1996.

Abstract: This paper is intended to show how non-trivial problems can be specified and solved in Martin-Löf's Type Theory. A particular class of problems is considered which contains some game problems.

S. Valentini, Extensionality versus constructivity

Mathematical Logic Quarterly.

Abstract: We will analyze some extensions of Martin-Löf's constructive type theory by means of extensional set constructors and we will show that often the most natural requirements over them lead to classical logic or even to inconsistency.