Author name cluster

Silvio Valentini

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

1 author row

I&C Journal 2003 Journal Article

A binary modal logic for the intersection types of lambda-calculus

Silvio Valentini
Matteo Viale

Intersection types discipline allows to define a wide variety of models for the type free lambda-calculus, but the Curry–Howard isomorphism breaks down for this kind of type systems. In this paper we show that the correspondence between types and suitable logical formulas can still be recovered appealing to the fact that there is a strict connection between the semantics for lambda-calculus induced by the intersection types and a Kripke-style semantics for modal and relevant logics. Indeed, we present a modal logic hinted by the analysis of the sub-typing relation for intersection types, and we show that the deduction relation for such a modal system is a conservative extension of the relation of sub-typing. Then, we define a Kripke-style semantics for the formulas of such a system, present suitable sequential calculi, prove a completeness theorem and give a syntactical proof of the cut elimination property. Finally, we define a decision procedure for theorem-hood and we show that it yields the finite model property and cut-redundancy.

Details DOI

TCS Journal 2003 Journal Article

A cartesian closed category in Martin-Löf's intuitionistic type theory

Silvio Valentini

First, we briefly recall the main definitions of the theory of Information Bases and Translations. These mathematical structures are the basis to construct the cartesian closed category InfBas, which is equivalent to the category ScDom of Scott domains. Then, we will show that all the definitions and the proof of all the properties that one needs in order to show that InfBas is indeed a cartesian closed category can be formalized within Martin-Löf's intuitionistic type theory.

Details DOI

TCS Journal 1996 Journal Article

Constructive domain theory as a branch of intuitionistic pointfree topology

Giovanni Sambin
Silvio Valentini
Paolo Virgili

In this paper, the notions of information base and of translation between information bases are introduced; they have a very simple intuitive interpretation and can be taken as an alternative approach to domain theory. Technically, they form a category which is equivalent to the category of Scott domains and approximable mappings. All the definitions and most of the results are inspired by the intuitionistic approach to pointfree topology as developed mainly by Martin-Löf and the first author. As in intuitionistic pointfree topology, constructivity is guaranteed by adopting the framework of Martin-Löfs intuitionistic type theory, equipped with a few abbreviations which allow to use a standard set theoretic notation.

Details DOI