4 papers
Dependently Sorted Nominal Signatures
Maribel Fernández, Miguel Pagano, Nora Szasz +1
We investigate an extension of nominal many-sorted signatures in which abstraction has a form of instantiation, called generalised concretion, as elimination operator (similarly to…
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…