Author name cluster

Eduardo Bonelli

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

CSL Conference 2023 Conference Paper

Reductions in Higher-Order Rewriting and Their Equivalence

Pablo Barenbaum
Eduardo Bonelli

Proof terms are syntactic expressions that represent computations in term rewriting. They were introduced by Meseguer and exploited by van Oostrom and de Vrijer to study equivalence of reductions in (left-linear) first-order term rewriting systems. We study the problem of extending the notion of proof term to higher-order rewriting, which generalizes the first-order setting by allowing terms with binders and higher-order substitution. In previous works that devise proof terms for higher-order rewriting, such as Bruggink’s, it has been noted that the challenge lies in reconciling composition of proof terms and higher-order substitution (β-equivalence). This led Bruggink to reject "nested" composition, other than at the outermost level. In this paper, we propose a notion of higher-order proof term we dub rewrites that supports nested composition. We then define two notions of equivalence on rewrites, namely permutation equivalence and projection equivalence, and show that they coincide.

Details

CSL Conference 2020 Conference Paper

Strong Bisimulation for Control Operators (Invited Talk)

Delia Kesner
Eduardo Bonelli
Andrés Viso

The purpose of this paper is to identify programs with control operators whose reduction semantics are in exact correspondence. This is achieved by introducing a relation ≃, defined over a revised presentation of Parigot’s λμ-calculus we dub ΛM. Our result builds on two fundamental ingredients: (1) factorization of λμ-reduction into multiplicative and exponential steps by means of explicit term operators of ΛM, and (2) translation of ΛM-terms into Laurent’s polarized proof-nets (PPN) such that cut-elimination in PPN simulates our calculus. Our proposed relation ≃ is shown to characterize structural equivalence in PPN. Most notably, ≃ is shown to be a strong bisimulation with respect to reduction in ΛM, i. e. two ≃-equivalent terms have the exact same reduction semantics, a result which fails for Regnier’s σ-equivalence in λ-calculus as well as for Laurent’s σ-equivalence in λμ.

Details

TCS Journal 2019 Journal Article

Typed path polymorphism

Mauricio Ayala-Rincón
Eduardo Bonelli
Juan Edi
Andrés Viso

Path polymorphism enables the definition of functions uniformly applicable to arbitrary recursively specified data structures. Path polymorphic function declarations rely on patterns of the form x y (i. e. the application of two variables), which decompose a data structure into its parts. We propose a static type system for a calculus that captures this feature, combining constants as types, union types and recursive types. The fundamental properties of Subject Reduction and Progress are addressed to guarantee well-behaved dynamics; they rely crucially on a novel notion of pattern compatibility. We also introduce an efficient type-checking algorithm by formulating a syntax-directed variant of the type system. This involves algorithms for checking type equivalence and subtyping, both based on coinductive characterizations of those relations.

Details DOI

TCS Journal 2017 Journal Article

On abstract normalisation beyond neededness

Eduardo Bonelli
Delia Kesner
Carlos Lombardi
Alejandro Ríos

We study normalisation of multistep strategies, strategies that reduce a set of redexes at a time, focusing on the notion of necessary sets, those which contain at least one redex that cannot be avoided in order to reach a normal form. This is particularly appealing in the setting of non-sequential rewrite systems, in which terms that are not in normal form may not have any needed redex. We first prove a normalisation theorem for abstract rewrite systems (ARS), a general rewriting framework encompassing many rewriting systems developed by P-A. Melliès [20]. The theorem states that multistep strategies reducing so called necessary and never-gripping sets of redexes at a time are normalising in any ARS. Gripping refers to an abstract property reflecting the behaviour of higher-order substitution. We then apply this result to the particular case of PPC, a calculus of patterns and to the lambda-calculus with parallel-or.

Details DOI

TCS Journal 2005 Journal Article

Normalisation for higher-order calculi with explicit substitutions

Eduardo Bonelli

Explicit substitutions (ES) were introduced as a bridge between the theory of rewrite systems with binders and substitution, such as the λ -calculus, and their implementation. In a seminal paper Melliès observed that the dynamical properties of a rewrite system and its ES-based implementation may not coincide: he showed that a strongly normalising term (i. e. one which does not admit infinite derivations) in the λ -calculus may lose this status in its ES-based implementation. This paper studies normalisation for the latter systems in the general setting of higher-order rewriting: Based on recent work extending the theory of needed strategies to non-orthogonal rewrite systems we show that needed strategies normalise in the ES-based implementation of any orthogonal pattern higher-order rewrite system.

Details DOI

MFCS Conference 2004 Invited Paper

Boxed Ambients with Communication Interfaces

Eduardo Bonelli
Adriana B. Compagnoni
Mariangiola Dezani-Ciancaglini
Pablo Garralda

Abstract We define BACI (Boxed Ambients with Communication Interfaces), an ambient calculus allowing a liberal communication policy. Each ambient carries its local view of the topic of conversation (the type of the information being exchanged) with parents and children that will condition where it is allowed to stay or migrate to and which ambients may be allowed to enter it. The topic of conversation view of ambients can dynamically change during migration. BACI is flexible enough to allow different topics of conversation between an ambient and different parents, without compromising type-safety: it uses port names for communication and ambient names for mobility. Capabilities and co-capabilities exchange port names and run-time typing information to control mobility. We show the type-soundness of BACI proving that it satisfies the subject reduction property. Moreover we study its behavioural semantics by means of a labelled transition system.

Details

CSL Conference 1999 Conference Paper

Using Fields and Explicit Substitutions to Implement Objects and Functions in a de Bruijn Setting

Eduardo Bonelli

Abstract We propose a calculus of explicit substitutions with de Bruijn indices for implementing objects and functions which is confluent and preserves strong normalization. We start from Abadi and Cardelli’s ς-calculus [ 1 ] for the object calculus and from the λ ν -calculus [ 20 ] for the functional calculus. The de Bruijn setting poses problems when encoding the λ ν -calculus within the ς-calculus following the style proposed in [ 1 ]. We introduce fields as a primitive construct in the target calculus in order to deal with these difficulties. The solution obtained greatly simplifies the one proposed in [ 17 ] in a named variable setting. We also eliminate the conditional rules present in the latter calculus obtaining in this way a full non-conditional first order system.

Details