3 citations · 5 across the 9 of their papers we have counts for
12 papers
Nominal Equational Rewriting and Narrowing
Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho +1
Narrowing is a well-known technique that adds to term rewriting mechanisms the required power to search for solutions to equational problems. Rewriting and narrowing are well-studi…
Nominal Equational Narrowing: Rewriting for Unification in Languages with Binders
Maribel Fernández, Daniele Nantes-Sobrinho, Daniella Santaguida
Narrowing extends term rewriting with the ability to search for solutions to equational problems. While first-order rewriting and narrowing are well studied, significant challenges…
Equational Reasoning Modulo Commutativity in Languages with Binders (Extended Version)
Ali K. Caires-Santos, Maribel Fernández, Daniele Nantes-Sobrinho
Many formal languages include binders as well as operators that satisfy equational axioms, such as commutativity. Here we consider the nominal language, a general formal framework…
Generalization Problems with Atom-Variables in Languages with Binders and Equational Theories
Daniele Nantes-Sobrinho, Manfred Schmidt-Schauss, Alexander Baumgartner +1
Generalization problems in languages with binders involve computing the most common structure between expressions while respecting bound variable renaming and freshness constraints…
Typed Non-determinism in Concurrent Calculi: The Eager Way
Bas van den Heuvel, Daniele Nantes-Sobrinho, Joseph W. N. Paulus +1
We consider the problem of designing typed concurrent calculi with non-deterministic choice in which types leverage linearity for controlling resources, thereby ensuring strong cor…
Strong Nominal Semantics for Fixed-Point Constraints
Ali K. Caires-Santos, Maribel Fernández, Daniele Nantes-Sobrinho
Nominal algebra includes -equality and freshness constraints on nominal terms endowed with a nominal set semantics that facilitates reasoning about languages with binders. Nomin…
Termination in Concurrency, Revisited
Joseph W. N. Paulus, Jorge A. Pérez, Daniele Nantes-Sobrinho
Termination is a central property in sequential programming models: a term is terminating if all its reduction sequences are finite. Termination is also important in concurrency in…
Typed Non-determinism in Functional and Concurrent Calculi
Bas van den Heuvel, Joseph W. N. Paulus, Daniele Nantes-Sobrinho +1
We study functional and concurrent calculi with non-determinism, along with type systems to control resources based on linearity. The interplay between non-determinism and linearit…
Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes (Extended Version)
Joseph W. N. Paulus, Daniele Nantes-Sobrinho, Jorge A. Pérez
Type-preserving translations are effective rigorous tools in the study of core programming calculi. In this paper, we develop a new typed translation that connects sequential and c…
Non-Deterministic Functions as Non-Deterministic Processes (Extended Version)
Joseph W. N. Paulus, Daniele Nantes-Sobrinho, Jorge A. Pérez
We study encodings of the lambda-calculus into the pi-calculus in the unexplored case of calculi with non-determinism and failures. On the sequential side, we consider lambdafail,…
On Nominal Syntax and Permutation Fixed Points
Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho
We propose a new axiomatisation of the alpha-equivalence relation for nominal terms, based on a primitive notion of fixed-point constraint. We show that the standard freshness rela…
Nominal C-Unification
Mauricio Ayala-Rincón, Washington de Carvalho-Segundo, Maribel Fernández +1
Nominal unification is an extension of first-order unification that takes into account the α-equivalence relation generated by binding operators, following the nominal approach. We…