6 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…
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…