Author name cluster

G. Castagna

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.

2 papers

1 author row

I&C Journal 2005 Journal Article

The Seal Calculus

G. Castagna
J. Vitek
F. Zappa Nardelli

The Seal Calculus is a process language for describing mobile computation. Threads and resources are tree structured; the nodes thereof correspond to agents, the units of mobility. The Calculus extends a π-calculus core with synchronous, objective mobility of agents over channels. This paper systematically compares all previous variants of Seal Calculus. We study their operational behaviour with labelled transition systems and bisimulations; by comparing the resulting algebraic theories we highlight the differences between these apparently similar approaches. This leads us to identify the dialect of Seal that is most amenable to operational reasoning and can form the basis of a distributed programming language. We propose type systems for characterising the communications in which an agent can engage. The type systems thus enforce a discipline of agent mobility, since the latter is coded in terms of higher-order communication.

Details DOI

I&C Journal 1995 Journal Article

A Calculus for Overloaded Functions with Subtyping

G. Castagna
G. Ghelli
G. Longo

We present a simple extension of typed λ-calculus where functions can be overloaded by putting different "branches of code" together. When the function is applied, the branch to execute is chosen according to a particular selection rule which depends on the type of the argument. The crucial feature of the present approach is that the branch selection depends on the "run-time type" of the argument, which may differ from its compile-time type, because of the existence of a subtyping relation among types. Hence overloading cannot be eliminated by a static analysis of code, but it is an essential feature to be dealt with during computation. We obtain in this way a type-dependent calculus, which differs from the various λ-calculi where types to not play any role during computation. We prove confluence and a generalized subject-reduction theorem for this calculus. We prove strong normalization for a "stratified" subcalculus. The definition of this calculus is guided by the understanding of object-oriented features and the connections between our calculus and object-orientedness are extensive stressed. We show that this calculus provides a foundation for types object-oriented languages which solves some of the problems of the standard record-based approach.

Details DOI