Colour refinement is at the heart of all the most efficient graph isomorphism software packages. In this paper we present a method for extending the applicability of refinement algorithms to directed graphs with weighted edges. We use {Traces} as a reference software, but the proposed solution is easily transferrable to any other refinement-based graph isomorphism tool in the literature. We substantiate the claim that the performances of the original algorithm remain substantially unchanged by showing experiments for some classes of benchmark graphs.

We are very proud and honoured to dedicate this volume to Corrado Böhm, who has been for us a teacher, mentor, colleague, and friend. But most of all, he was a brilliant role-model to follow.

This paper presents a novel method for comparing computational properties of λ-terms that are typeable with intersection types, with respect to terms that are typeable with Curry types. We introduce a translation from intersection typing derivations to Curry typeable terms that is preserved by β-reduction: this allows the simulation of a computation starting from a term typeable in the intersection discipline by means of a computation starting from a simply typeable term. Our approach proves strong normalisation for the intersection system naturally by means of purely syntactical techniques. The paper extends the results presented in Bucciarelli et al. (1999) to the whole intersection type system of Barendregt, Coppo and Dezani, thus providing a complete proof of the conjecture, proposed in Leivant (1990), that all functions uniformly definable using intersection types are already definable using Curry types.

No abstract available.

Some λ-terms exhibit the following alternation property: whenever a redex having the shape (λx.P) (λy.Q) is created in a reduction path starting with the contraction of M N, then either λx appears in M and λy in N, or λx appears in N and λy in M. In this paper, we investigate the alternation property and we establish its relevance in the context of typed calculi. In particular, we prove that the alternation property implies normalization. To this aim, we use a simple technique based on labels. The intended meaning of the labelling is to give information about the minimal number of contractions needed by a variable to be substituted during the reduction process. Further, we apply this result to obtain new normalization proofs for Curry's simply typed lambda calculus and, similarly, for terms typable with intersection types.

This paper presents a new method for comparing computation-properties of /spl lambda/-terms typeable with intersection types with respect to terms typeable with Curry types. In particular, strong normalization and /spl lambda/-definability are investigated. A translation is introduced from intersection typing derivations to Curry typeable terms; the main feature of the proposed technique is that the translation is preserved by /spl beta/-reduction. This allows to simulate a computation starting from a term typeable in the intersection discipline by means of a computation starting from a simply typeable term. Our approach naturally leads to prove strong normalization in the intersection system by means of purely syntactical techniques. In addition, the presented method enables us to give a proof of a conjecture proposed by Leivant in 1990, namely that all functions uniformly definable using intersection types are already definable using Curry types.

Type-free lazy $\lambda$-calculus is enriched with angelic parallelism and demonic nondeterminism. Call-by-name and call-by-value abstractions are considered and the operational semantics is stated in terms of a must convergence predicate. We introduce a type assignment system with intersection and union types, and we prove that the induced logical semantics is fully abstract.

An investigation on the interaction between /spl beta/-reduction and /spl eta/-expansion is provided in a labelled /spl lambda/-calculus, where additional information, that is constituted by integers, can be considered as a type in an abstract sense. This leads to propose the splitting of the /spl beta/-rule into two parts: a restricted /spl beta/-rule (/spl beta//sup +/), strongly normalizing, and a reversed /spl eta/-rule (/spl eta//sup -/), which comes out to have different computational interpretations for reduction in untyped and typed calculi (static and dynamic allocation of computation resources, respectively). To motivate the opportunity of this splitting, the paper hints to new proofs of strong normalization theorems for some typed /spl lambda/-calculi in Curry style.

The polymorphic type assignment system F/sub 2/ is the type assignment counterpart of Girard's and Reynolds' (1972) system F. Though introduced in the early seventies, both the type inference and the type checking problems for F/sub 2/ remained open for a long time. Recently, an undecidability result was announced. Consequently, it is considerably interesting to find decidable restrictions of the system. We show a bounded type inference and a bounded type checking algorithm, both based on the study of the relationship between the typability of a term and the typability of terms that "properly" /spl eta/-reduce to it.>

Retractions existing in all models of simply typed lambda -calculus are studied and related to other relations among types, such as isomorphisms, surjections, and injections. A formal system to deduce the existence of such retractions is shown to be sound and complete with respect to retractions definable by linear lambda -terms. Results aiming at a system complete with respect to the provable retractions tout court are established.>

Given a finite set T identical to (T/sub 1/, . . . ,T/sub t/) of terms of the lambda - beta -K-calculus and a set X/sub T/ identical to (x/sub 1/, . . ., x/sub n/) of free variables (occurring in the elements of T), X/sub T/-separability is the problem of deciding whether there exists a simultaneous substitution for the elements of X/sub T/ transforming T into the set Z identical to (Z/sub 1/, . . . Z/sub t/) of arbitrary terms. The X/sub T/-separability problem is proved to be solvable for any approximation T/sup Hash / of the set T by terms in lambda - beta - Omega -normal form. Since the characterization is constructive, if the terms T/sup , Hash //sub i/ identical to lambda x/sub 1/ . . . x/sub n/. T/sup Hash //sub i/ (i=1, . . ., t) are closed then the sequence T/sup Hash //sub 1/, . . ., T/sup Hash //sub t/ induces a family of mappings (from n to t dimensions) whose surjectivity and right-invertibility becomes decidable. The left-invertibility of this family is proved to be decidable too.>