Reduction of the Intruder Deduction Problem into Equational Elementary Deduction for Electronic Purse Protocols with Blind Signatures. - Daniele Nantes Sobrinho; Mauricio Ayala-Rincón (WoLLIC, 2010)

Elementary Deduction Problem for Locally Stable Theories with Normal Forms - Mauricio Ayala-Rincón; Maribel Fernández; Daniele Nantes Sobrinho (LSFA, 2012)

O problema da dedução do intruso para teorias AC-convergentes localmente estáveis. - Daniele Nantes Sobrinho (2013)

Nominal Narrowing. - Mauricio Ayala-Rincón; Maribel Fernández; Daniele Nantes-Sobrinho (FSCD, 2016)

A Formalisation of Nominal α-equivalence with A and AC Function Symbols. - Mauricio Ayala-Rincón; Washington de Carvalho Segundo; Maribel Fernández; Daniele Nantes-Sobrinho (LSFA, 2016)

On Solving Nominal Fixpoint Equations. - Mauricio Ayala-Rincón; Washington de Carvalho Segundo; Maribel Fernández; Daniele Nantes-Sobrinho (FroCoS, 2017)

Nominal C-Unification. - Mauricio Ayala-Rincón; Washington de Carvalho Segundo; Maribel Fernández; Daniele Nantes-Sobrinho (LOPSTR, 2017)

Intruder deduction problem for locally stable theories with normal forms and inverses. - Mauricio Ayala-Rincón; Maribel Fernández; Daniele Nantes-Sobrinho (Theor. Comput. Sci., 2017)

Relating Process Languages for Security and Communication Correctness (Extended Abstract). - Daniele Nantes; Jorge A. Pérez 001 (FORTE, 2018)

Fixed-Point Constraints for Nominal Equational Unification. - Mauricio Ayala-Rincón; Maribel Fernández; Daniele Nantes-Sobrinho (FSCD, 2018)

A Formalisation of Nominal C-Matching through Unification with Protected Variables. - Mauricio Ayala-Rincón; Washington de Carvalho Segundo; Maribel Fernández; Daniele Nantes-Sobrinho (LSFA, 2018)

Brasilia Spring on Automated Reasoning. - Cláudia Nalon; Daniele Nantes Sobrinho; Elaine Pimentel; João Marcos 001 (ACM SIGLOG News, 2018)

A Certified Functional Nominal C-Unification Algorithm. - Mauricio Ayala-Rincón; Maribel Fernández; Gabriel Ferreira Silva; Daniele Nantes-Sobrinho (LOPSTR, 2019)

On Solving Nominal Disunification Constraints. - Mauricio Ayala-Rincón; Maribel Fernández; Daniele Nantes-Sobrinho; Deivid Vale (LSFA, 2019)

A formalisation of nominal α-equivalence with A, C, and AC function symbols. - Mauricio Ayala-Rincón; Washington de Carvalho Segundo; Maribel Fernández; Daniele Nantes-Sobrinho; Ana Cristina Rocha Oliveira (Theor. Comput. Sci., 2019)

An Investigation into General Nominal Equational Problems (Work in progress). - Mauricio Ayala-Rincón; Maribel Fernández; Daniele Nantes-Sobrinho; Deivid Vale (UNIF, 2020)

A, C, and AC Nominal Anti-Unification. - Alexander Baumgartner; Daniele Nantes-Sobrinho (UNIF, 2020)

On Nominal Syntax and Permutation Fixed Points. - Mauricio Ayala-Rincón; Maribel Fernández; Daniele Nantes-Sobrinho (Log. Methods Comput. Sci., 2020)

Nominal Equational Problems. - Mauricio Ayala-Rincón; Maribel Fernández; Daniele Nantes-Sobrinho; Deivid Vale (FoSSaCS, 2021)

Non-Deterministic Functions as Non-Deterministic Processes. - Joseph W. N. Paulus; Daniele Nantes-Sobrinho; Jorge A. Pérez 001 (FSCD, 2021)

Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes. - Joseph W. N. Paulus; Daniele Nantes-Sobrinho; Jorge A. Pérez 001 (TYPES, 2021)

A subexponential view of domains in session types. - Daniele Nantes; Carlos Olarte; Daniel Ventura (LSFA, 2021)

Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes (Extended Version). - Joseph W. N. Paulus; Daniele Nantes-Sobrinho; Jorge A. Pérez 001 (CoRR, 2021)

Formalising nominal C-unification generalised with protected variables. - Mauricio Ayala-Rincón; Washington de Carvalho Segundo; Maribel Fernández; Gabriel Ferreira Silva; Daniele Nantes-Sobrinho (Math. Struct. Comput. Sci., 2021)

A Certified Algorithm for AC-Unification. - Mauricio Ayala-Rincón; Maribel Fernández; Gabriel Ferreira Silva; Daniele Nantes Sobrinho (FSCD, 2022)

Nominal Anti-Unification with Atom-Variables. - Manfred Schmidt-Schauß; Daniele Nantes-Sobrinho (FSCD, 2022)

Functions as Processes: The Case of Collapsing Non-determinism. - Bas van den Heuvel 001; Joseph W. N. Paulus; Daniele Nantes-Sobrinho; Jorge A. Pérez 001 (CoRR, 2022)

Typed Non-determinism in Functional and Concurrent Calculi. - Bas van den Heuvel 001; Joseph W. N. Paulus; Daniele Nantes-Sobrinho; Jorge A. Pérez 001 (APLAS, 2023)

Towards Fast Nominal Anti-unification of Letrec-Expressions. - Manfred Schmidt-Schauß; Daniele Nantes-Sobrinho (CADE, 2023)

Nominal AC-Matching. - Mauricio Ayala-Rincón; Maribel Fernández; Gabriel Ferreira Silva; Temur Kutsia; Daniele Nantes-Sobrinho (CICM, 2023)

Termination in Concurrency, Revisited. - Joseph W. N. Paulus; Jorge A. Pérez 001; Daniele Nantes-Sobrinho (PPDP, 2023)

Non-Deterministic Functions as Non-Deterministic Processes (Extended Version). - Joseph W. N. Paulus; Daniele Nantes-Sobrinho; Jorge A. Pérez 001 (Log. Methods Comput. Sci., 2023)

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning. - Andreas Lööw; Daniele Nantes-Sobrinho; Sacha-Élie Ayoun; Caroline Cronjäger; Petar Maksimovic 001; Philippa Gardner (ECOOP, 2024)

Matching Plans for Frame Inference in Compositional Reasoning. - Andreas Lööw; Daniele Nantes-Sobrinho; Sacha-Élie Ayoun; Petar Maksimovic 001; Philippa Gardner (ECOOP, 2024)

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Extended Version). - Andreas Lööw; Daniele Nantes-Sobrinho; Sacha-Élie Ayoun; Caroline Cronjäger; Petar Maksimovic 001; Philippa Gardner (CoRR, 2024)

Strong Nominal Semantics for Fixed-Point Constraints. - Ali K. Caires-Santos; Maribel Fernández; Daniele Nantes-Sobrinho (CoRR, 2024)

Typed Non-determinism in Concurrent Calculi: The Eager Way. - Bas van den Heuvel 001; Daniele Nantes-Sobrinho; Joseph W. N. Paulus; Jorge A. Pérez 001 (CoRR, 2024)

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact). - Andreas Lööw; Daniele Nantes-Sobrinho; Sacha-Élie Ayoun; Caroline Cronjäger; Nat Karmios; Petar Maksimovic 001; Philippa Gardner (Dagstuhl Artifacts Ser., 2024)

Nominal Equational Rewriting and Narrowing. - Mauricio Ayala-Rincón; Maribel Fernández; Daniele Nantes-Sobrinho; Daniella Santaguida (LSFA, 2024)

Report on WiL 2024. - Daniele Nantes-Sobrinho; Elaine Pimentel; Tephilla Prince (ACM SIGLOG News, 2024)

Certified First-Order AC-Unification and Applications. - Mauricio Ayala-Rincón; Maribel Fernández; Gabriel Ferreira Silva; Temur Kutsia; Daniele Nantes-Sobrinho (J. Autom. Reason., 2024)

Equational Reasoning Modulo Commutativity in Languages with Binders. - Ali K. Caires-Santos; Maribel Fernández; Daniele Nantes-Sobrinho (CADE, 2025)

Equational Reasoning Modulo Commutativity in Languages with Binders (Extended Version). - Ali K. Caires-Santos; Maribel Fernández; Daniele Nantes-Sobrinho (CoRR, 2025)

Generalization Problems with Atom-Variables in Languages with Binders and Equational Theories. - Daniele Nantes-Sobrinho; Manfred Schmidt-Schauß; Alexander Baumgartner; Temur Kutsia (CoRR, 2025)

Correction to: Certified First-Order AC-Unification and Applications. - Mauricio Ayala-Rincón; Maribel Fernández; Gabriel Ferreira Silva; Temur Kutsia; Daniele Nantes-Sobrinho (J. Autom. Reason., 2025)

Nominal Equational Narrowing: Rewriting for Unification in Languages with Binders. - Maribel Fernández; Daniele Nantes-Sobrinho; Daniella Santaguida (CoRR, 2025)

Compositional Symbolic Execution for the Next 700 Memory Models (Extended Version). - Andreas Lööw; Seung Hoon Park; Daniele Nantes-Sobrinho; Sacha-Élie Ayoun; Opale Sjöstedt; Philippa Gardner (CoRR, 2025)