Author name cluster

Roberto Di Cosmo

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.

7 papers

2 author rows

I&C Journal 2014 Journal Article

Aeolus: A component model for the cloud

Roberto Di Cosmo
Jacopo Mauro
Stefano Zacchiroli
Gianluigi Zavattaro

We introduce the Aeolus component model, which is specifically designed to capture realistic scenarios arising when configuring and deploying distributed applications in the so-called cloud environments, where interconnected components can be deployed on clusters of heterogeneous virtual machines, which can be in turn created, destroyed, and connected on-the-fly. The full Aeolus model is able to describe several component characteristics such as dependencies, conflicts, non-functional requirements (replication requests and load limits), as well as the fact that component interfaces to the world might vary depending on the internal component state. When the number of components needed to build an application grows, it becomes important to be able to automate activities such as deployment and reconfiguration. This corresponds, at the level of the model, to the ability to decide whether a desired target system configuration is reachable, which we call the achievability problem, and producing a path to reach it. In this work we show that the achievability problem is undecidable for the full Aeolus model, a strong limiting result for automated configuration in the cloud. We also show that the problem becomes decidable, but Ackermann-hard, as soon as one drops non-functional requirements. Finally, we provide a polynomial time algorithm for the further restriction of the model where support for inter-component conflicts is also removed.

Details DOI

CSL Conference 2008 Conference Paper

On Isomorphisms of Intersection Types

Mariangiola Dezani-Ciancaglini
Roberto Di Cosmo
Elio Giovannetti
Makoto Tatsuta

Abstract The study of type isomorphisms for different λ -calculi started over twenty years ago, and a very wide body of knowledge has been established, both in terms of results and in terms of techniques. A notable missing piece of the puzzle was the characterization of type isomorphisms in the presence of intersection types. While at first thought this may seem to be a simple exercise, it turns out that not only finding the right characterization is not simple, but that the very notion of isomorphism in intersection types is an unexpectedly original element in the previously known landscape, breaking most of the known properties of isomorphisms of the typed λ -calculus. In particular, types that are equal in the standard models of intersection types may be non-isomorphic.

Details

LPAR Conference 2004 Conference Paper

The Equational Theory of < N, 0, 1, +, ×, uparrow > Is Decidable, but Not Finitely Axiomatisable

Roberto Di Cosmo
Thomas Dufour

Abstract In 1969, Tarski asked whether the arithmetic identities taught in high school are complete for showing all arithmetic equations valid for the natural numbers. We know the answer to this question for various subsystems obtained by restricting in different ways the language of arithmetic expressions, yet, up to now we knew nothing of the original system that Tarski considered when he started all this research, namely the theory of integers under sum, product, exponentiation with two constants for zero and one. This paper closes this long standing open problem, by providing an elementary proof, relying on previous work of R. Gurevič, of the fact that Tarski’s original system is decidable, yet not finitely aximatisable. We also show some consequences of this result for the theory of isomorphisms of types.

Details

LPAR Conference 2000 Conference Paper

Playing Logic Programs with the Alpha-Beta Algorithm

Jean-Vincent Loddo
Roberto Di Cosmo

Abstract Alpha-Beta is a well known optimized algorithm used to compute the values of classical combinatorial games, like chess and checkers The known proofs of correctness of Alpha-Beta do rely on very specific properties of the values used in the classical context (integers or reals), and on the finiteness of the game tree. In this paper we prove that Alpha-Beta correctly computes the value of a game tree even when these values are chosen in a much wider set of partially ordered domains, which can be pretty far apart from integer and reals, like in the case of the lattice of idempotent substitutions or ex-equations used in logic programming. We do so in a more general setting that allows us to deal with infinite games, and we actually prove that for potentially infinite games Alpha-Beta correctly computes the value of the game whenever it terminates. This correctness proofs allows us to apply Alpha-Beta to new domains, like constraint logic programming.

Details

CSL Conference 1999 Conference Paper

A Linear Logical View of Linear Type Isomorphisms

Vincent Balat
Roberto Di Cosmo

Abstract The notion of isomorphisms of types has many theoretical as well as practical consequences, and isomorphisms of types have been investigated at length over the past years. Isomorphisms in weak system (like linear lambda calculus) have recently been investigated due to their practical interest in library search. In this paper we give a remarkably simple and elegant characterization of linear isomorphisms in the setting of Multiplicative Linear Logic (MLL), by making an essential use ofthe correctness criterion for Proof Nets due to Girard.

Details

TCS Journal 1996 Journal Article

Combining algebraic rewriting, extensional lambda calculi, and fixpoints

Roberto Di Cosmo
Delia Kesner

It is well known that confluence and strong normalization are preserved when combining algebraic rewriting systems with the simply typed lambda calculus. It is equally well known that confluence fails when adding either the usual contraction rule for η, or recursion together with the usual contraction rule for surjective pairing. We show that confluence and strong normalization are modular properties for the combination of algebraic rewriting systems with typed lambda calculi enriched with expansive extensional rules for η and surjective pairing. We also show how to preserve confluence in a modular way when adding fixpoints to different rewriting systems. This result is also obtained by a simple translation technique allowing to simulate bounded recursion.

Details DOI

CSL Conference 1996 Conference Paper

Rewriting with Extensional Polymorphic Lambda-Calculus

Roberto Di Cosmo
Delia Kesner

Abstract We provide a confluent and strongly normalizing rewriting system, based on expansion rules, for the extensional second order typed lambda calculus with product and unit types: this system corresponds to the Intuitionistic Positive Calculus with implication, conjunction, quantification over proposition and the constant True. This result is an important step towards a new theory of reduction based on expansion rules, and gives a natural interpretation to the notion of second order η-long normal forms used in higher order resolution and unification, that are here just the normal forms of our reduction system.

Details