Author name cluster

Giorgio 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.

11 papers

1 author row

TCS Journal 2026 Journal Article

Elimination of annotation dependencies in validation for Modern JSON Schema

Lyes Attouche
Mohamed-Amine Baazizi
Dario Colazzo
Giorgio Ghelli
Stefan Klessinger
Carlo Sartiani
Stefanie Scherzinger

JSON Schema is a logical language used to define the structure of JSON values. JSON Schema syntax is based on nested schema objects. In all versions of JSON Schema until Draft-07, collectively known as Classical JSON Schema, the semantics of a schema was entirely described by the set of JSON values that it validates. This semantics was the basis for a thorough theoretical study and for the development of tools to decide satisfiability and equivalence of schemas. Unfortunately, Classical JSON Schema suffered a severe limitation in its ability to express extensions of object schemas, which caused the introduction, with Draft 2019-09, of two disruptive features: annotation dependency and dynamic references. These new features undermine the previously developed semantic theory, and the algorithms used to decide satisfiability for Classical JSON Schema are not easy to extend. One possible solution is rewriting a schema written in Modern JSON Schema into an equivalent schema in Classical JSON Schema. In this paper we prove that the elimination of annotation dependent keywords cannot, in general, avoid an exponential increase of the schema dimension. We provide an algorithm to eliminate these keywords that, despite the theoretical lower bound, behaves quite well in practice, as we verify with an extensive set of experiments.

Details DOI

TCS Journal 2023 Journal Article

Negation-closure for JSON Schema

Mohamed-Amine Baazizi
Dario Colazzo
Giorgio Ghelli
Carlo Sartiani
Stefanie Scherzinger

JSON Schema is an evolving standard for describing families of JSON documents. It is a logical language, based on a set of assertions that describe features of the JSON value under analysis and on logical or structural combinators for these assertions, including a negation operator. Most logical languages with negation enjoy negation closure: for every operator, they have a negation-dual that allows negation to be pushed through the operator. We show that this is not the case for JSON Schema, study how that changed with the latest versions of the Draft, and discuss how the language may be enriched accordingly. To this aim, we exploit an algebraic reformulation of JSON Schema, which is helpful for the formal manipulation of the language.

Details DOI

I&C Journal 2007 Journal Article

Expressiveness and complexity of graph logic

Anuj Dawar
Philippa Gardner
Giorgio Ghelli

We investigate the complexity and expressive power of a spatial logic for reasoning about graphs. This logic was previously introduced by Cardelli, Gardner and Ghelli, and provides the simplest setting in which to explore such results for spatial logics. We study several forms of the logic: the logic with and without recursion, and with either an exponential or a linear version of the basic composition operator. We study the combined complexity and the expressive power of the four combinations. We prove that, without recursion, the linear and exponential versions of the logic correspond to significant fragments of first-order (FO) and monadic second-order (MSO) Logics; the two versions are actually equivalent to FO and MSO on graphs representing strings. However, when the two versions are enriched with μ-style recursion, their expressive power is sharply increased. Both are able to express PSPACE-complete problems, although their combined complexity and data complexity still belong to PSPACE.

Details DOI

I&C Journal 2005 Journal Article

Secrecy and group creation

Luca Cardelli
Giorgio Ghelli
Andrew D. Gordon

We add an operation of group creation to the typed π-calculus, where a group is a type for channels. Creation of fresh groups has the effect of statically preventing certain communications, and can block the accidental or malicious leakage of secrets. Intuitively, no channel belonging to a fresh group can be received by processes outside the initial scope of the group, even if those processes are untyped. We formalize this intuition by adapting a notion of secrecy introduced by Abadi, and proving a preservation of secrecy property.

Details DOI

I&C Journal 2005 Journal Article

Subtyping recursion and parametric polymorphism in kernel fun

Dario Colazzo
Giorgio Ghelli

We study subtype checking for recursive types in system kernel Fun, a typed λ-calculus with subtyping and bounded second-order polymorphism. Along the lines of [ACM Transactions on Programming Languages and Systems, 15(4), (1993) 575], we define a subtype relation over kernel Fun recursive types, and prove it to be transitive. We then show that the natural extension of the algorithm introduced in [loc. cit] to compare first-order recursive types yields a non complete algorithm. Finally, we prove the completeness and correctness of a different algorithm, which lends itself to efficient implementations.

Details DOI

I&C Journal 2002 Journal Article

Foundations for Extensible Objects with Roles

Giorgio Ghelli

Object-oriented database systems are an emerging, promising technology, underpinned by the integration of ideas from object-oriented languages along with the specific needs of database applications. The fundamental reason for using such systems is that any real-world entity can be modeled by one object which matches its structure and behavior. To this end, the standard notion of object must be augmented so that it can model the fact that an entity may acquire new pieces of structure and behavior during its existence without changing its identity. To allow this extensibility in a statically typed system, a notion of context-dependent behavior (role playing) must be added to the basic features of object-oriented languages. This feature is also a useful modeling device. Languages with role mechanisms have already been proposed. However, their design is full of choices which cannot be easily justified. A strong foundation for the object-with-roles notion would be extremely helpful to justify these choices and to understand, and prove, the properties of such a mechanism. In this paper we describe such a foundation, building on the object model proposed by Abadi and Cardelli.

Details DOI

I&C Journal 2002 Journal Article

Types for the Ambient Calculus

Luca Cardelli
Giorgio Ghelli
Andrew D. Gordon

The ambient calculus is a concurrent calculus where the unifying notion of ambient is used to model many different constructs for distributed and mobile computation. We study a type system that describes several properties of ambient behavior. The type system allows ambients to be partitioned in disjoint sets (groups), according to the intended design of a system, in order to specify both the communication and the mobility behavior of ambients.

Details DOI

I&C Journal 1999 Journal Article

Basic Theory of F-Bounded Quantification

Paolo Baldan
Giorgio Ghelli
Alessandra Raffaetà

System F-bounded is a second-order typed lambda calculus, where the basic features of object-oriented languages can be naturally modelled. F-bounded extends the better known system F ⩽, in a way that provides an immediate solution for the treatment of the so-called “binary methods. ” Although more powerful than F ⩽ and also quite natural, system F-bounded has only been superficially studied from a foundational perspective and many of its essential properties have been conjectured but never proved in the literature. The aim of this paper is to give a solid foundation to F-bounded, by addressing and proving the key properties of the system. In particular, transitivity elimination, completeness of the type checking semi-algorithm, the subject reduction property for βη reduction, conservativity with respect to system F ⩽, and antisymmetry of a “full” subsystem are considered, and various possible formulations for system F-bounded are compared. Finally, a semantic interpretation of system F-bounded is presented, based on partial equivalence relations.

Details DOI

TCS Journal 1998 Journal Article

Bounded existentials and minimal typing

Giorgio Ghelli
Benjamin Pierce

We study an extension of the second-order calculus of bounded quantification, System F ⩽, with bounded existential types. Surprisingly, the most natural formulation of this extension lacks the important minimal typing property of F ⩽, which ensures that the set of types possessed by a typeable term can be characterized by a single least element. We consider alternative formulations and give an algorithm computing minimal types for the slightly weaker Kernel Fun variant of F ⩽.

Details DOI

I&C Journal 1997 Journal Article

Termination of SystemF-bounded: A Complete Proof

Giorgio Ghelli

SystemF-bounded is a second-order typedλ-calculus with subtyping which has been defined to carry out foundational studies about the type systems of object-oriented languages. The almost recursive nature of the essential feature of this system makes one wonder whether it retains the strong normalization property, with respect to first- and second-orderβϵreduction of systemF ⩽. We prove that this is the case. The proof is carried out to the last detail to allow the reader to be convinced of its correctness.

Details DOI

TCS Journal 1995 Journal Article

Divergence of F⩽ type checking

Giorgio Ghelli

System F ⩽ is an extension of second-order typed lambda calculus, where a subtype hierarchy among types is defined, and bounded second-order lambda abstraction is allowed. This language is a basis for much of the current research on integration of typed functional languages with subtypes and inheritance. An algorithm to perform type checking for F ⩽ expressions has been known since the language Fun was defined. The algorithm has been proved complete, by the author and Curien, which means that it is a semi-decision procedure for the type-checking problem. In this paper we show that this algorithm is not a decision procedure, by exhibiting a term which makes it diverge. This result was the basis of Pierce's proof of undecidability of typing for F ⩽. We study the behavior of the algorithm to show that our diverging judgement is in some sense contained in any judgement which makes the algorithm diverge. On the basis of this result, and of other results in the paper, we claim that the chances that the algorithm will loop while type-checking a “real program” are negligible. Hence, the undecidability of F ⩽ type-checking should not be considered as a reason to prevent the adoption of F ⩽ as a basis for defining programming languages of practical interest. Finally, we show the undecidability of an important subsystem of F ⩽.

Details DOI