U. Solitro, S. Valentini, Toward Typed lambda-calculi for Linear Logic,

proceeding of "The Third Italian Conference on theoretical Computer Science" (ed. Bertoni, Bshm, Miglioli), World Scientific, Mantova 1989, pp. 413-424.

Abstract: In this paper it is studied the problem of stating a Curry-Howard isomorphism for Girard's Linear Logic. Two solutions are proposed: one for the intuitionistic variant of the logic and one for a subsytem of the logic which includes the multiplicative and exponential connectives. Different calculi have been developed for the two cases.

S. Valentini, The judgement calculus for Intuitionistic Linear Logic: proof theory and semantics,

Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, n. 38 (1992), pp. 39-58.

Abstract: In this paper I propose a new set of rules for a judgement calculus, i.e. a typed lambda calculus, based on Intuitionistic Linear Logic; these rules ease the problem of defining a suitable mathematical semantics. A proof of the canonical form theorem for this new system is given: it assures, beside the consistency of the calculus, the termination of the evaluation process of every well-typed element. The definition of the mathematical semantics and a completeness theorem, that turns out to be a representation theorem, follow. This semantics is the basis to obtain a semantics for the evaluation process of every well-typed program.

U. Solitro, S. Valentini, Local computation in linear logic,

Mathematical Logic Quarterly, n. 39 (1993), pp. 201-212.

Abstract: This work deals with the exponential fragment of Girard's linear logic without the contraction rule. This logical system has a natural relation with the direct logic . A new sequent calculus for this logic is presented in order to remove also the weakening rule and recover its behavior via a special treatment of the propositional constants; the process of cut-elimination can be performed using only "local" reductions. Hence a typed calculus, which admits only local rewriting rules, can be introduced in a natural manner. Its main properties --- normalizability and confluence --- has been investigated; moreover this calculus has been proved to satisfy a Curry-Howard isomorphism with respect to the logical system in question.

S. Valentini, A proof of the normal form theorem for the closed terms of Girard's System F by means of computability,

Mathematical Logic Quarterly, 39 (1993), pp. 539-544.

Abstract: In this paper a proof of the normal form theorem for the closed terms of Girard's system F is given by using a computability method à la Tait. It is worth noting that most of the standard consequences of the normal form theorem can be obtained using this version of the theorem as well. From the proof-theoretical point of view the interest of the proof is that the definition of computable derivation here used does not seem to be well founded.

S. Valentini, A note on a straightforward proof of normal form theorem for simply typed lambda-calculi,

Bollettino dell'Unione Matematica Italiana, 8-A (1994), pp. 207-213.

Abstract: Il lavoro presenta una nuova prova, basata su alcune idea di Martin-Löf e Tait, del ben noto teorema di forma normale per il lambda calcolo tipato semplice, la cui prima dimostrazione è dovuta a Turing. Il metodo di prova usato è molto semplice, ma al tempo stesso si presenta come molto generale e facilmente applicabile ad una varietà di lambda calcoli tipati.

S. Valentini, On the decidability of the equality theory of simply typed lambda-calculi,

Bollettino dell'Unione Matematica Italiana, 9-A (1995), pp. 83-93.

Abstract: Il lavoro presenta una nuova prova del ben noto risultato di decidibilità della teoria dell'ugualianza per un lambda-calcolo tipato semplice. La novità principale consiste nel fatto che per ottenere tale risultato non si fa ricorso al teorema di Church-Rosser come avviene nella prova usuale. Il metodo di prova usato è molto semplice, ma al tempo stesso si presenta come molto generale e facilmente applicabile ad una varietà di lambda calcoli tipati semplici.

V. Capretta, S. Valentini, A general method to prove the normalization theorem for first and second order typed lambda-calculi,

Mathematical Structures in Computer Science, 9, 1999, pp.719-739

Abstract: In this paper we describe a method to prove the normalization property for a large variety of typed lambda calculi of first and second order, based on a proof of equivalence of two deduction systems. We first illustrate the method on the elementary example of simply typed lambda calculus and then we show how to extend it to a more expressive dependent type system. Finally we use it to prove the normalization theorem for Girard's system F.

S. Valentini, An elementary proof of strong normalization for intersection types,

Archive for Mathematical Logic

Abstract: We provide a new and elementary proof of strong normalization for the lambda calculus of intersection types. It uses no strong method, like for instance Tait-Girard reducibility predicates, but just simple induction on type complexity and derivation length and thus it is obviously formalizable within first order arithmetic. To obtain this result, we introduce a new system for intersection types whose rules are directly inspired by the reduction relation. Finally, we show that not only the set of strongly normalizing terms of pure lambda calculus can be characterized in this system, but also that a straightforward modification of its rules allows to characterize the set of weakly normalizing terms.