Author name cluster

G. Ghelli

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

TCS Journal 2013 Journal Article

Efficient asymmetric inclusion of regular expressions with interleaving and counting for XML type-checking

D. Colazzo
G. Ghelli
L. Pardini
C. Sartiani

The inclusion of Regular Expressions (REs) is the kernel of any type-checking algorithm for XML manipulation languages. XML applications would benefit from the extension of REs with interleaving and counting, but this is not feasible in general, since inclusion is EXPSPACE-complete for such extended REs. In Colazzo et al. (2009) [1] we introduced a notion of “conflict-free REs”, which are extended REs with excellent complexity behaviour, including a polynomial inclusion algorithm [1] and linear membership (Ghelli et al. , 2008 [2]). Conflict-free REs have interleaving and counting, but the complexity is tamed by the “conflict-free” limitations, which have been found to be satisfied by the vast majority of the content models published on the Web. However, a type-checking algorithm needs to compare machine-generated subtypes against human-defined supertypes. The conflict-free restriction, while quite harmless for the human-defined supertype, is far too restrictive for the subtype. We show here that the PTIME inclusion algorithm can be actually extended to deal with totally unrestricted REs with counting and interleaving in the subtype position, provided that the supertype is conflict-free. This is exactly the expressive power that we need in order to use subtyping inside type-checking algorithms, and the cost of this generalized algorithm is only quadratic, which is as good as the best algorithm we have for the symmetric case (see [1]). The result is extremely surprising, since we had previously found that symmetric inclusion becomes NP-hard as soon as the candidate subtype is enriched with binary intersection, a generalization that looked much more innocent than what we achieve here.

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

I&C Journal 1994 Journal Article

Decidability and Confluence of βη top≤ Reduction in F≤

P.L. Curien
G. Ghelli

We contribute to the syntactic study of F ≤, a variant of second-order λ-calculus F which appears as a paradigmatic kernel language for polymorphism and subtyping. The type system of F ≤ has a maximum type Top and bounded quantification. We endow this language with the β-rules (for terms and types), to which we add η-rules (for terms and types) and a rule which equates all terms of type Top. These rules are suggested by the axiomatization of cartesian closed categories. We exhibit a weakly normalizing and confluent reduction system for this theory βη top≤, and show that it is decidable. It is also confluent, but decidability does not follow from confluence, since reduction is not effective. Our proofs rely on the confluence and decidability of a corresponding system on F 1 (the extension of F with a terminal type).

Details DOI