Formalizing the Confluence of Orthogonal Rewriting Systems - Ana Cristina Rocha Oliveira; Mauricio Ayala-Rincón (LSFA, 2012)

Checking Overlaps of Nominal Rewriting Rules. - Mauricio Ayala-Rincón; Maribel Fernández; Murdoch James Gabbay; Ana Cristina Rocha Oliveira (LSFA, 2015)

Completeness in PVS of a Nominal Unification Algorithm. - Mauricio Ayala-Rincón; Maribel Fernández; Ana Cristina Rocha Oliveira (LSFA, 2015)

Confluence of Orthogonal Term Rewriting Systems in the Prototype Verification System. - Ana Cristina Rocha Oliveira; André Luiz Galdino; Mauricio Ayala-Rincón (J. Autom. Reason., 2017)

Nominal essential intersection types. - Mauricio Ayala-Rincón; Maribel Fernández; Ana Cristina Rocha Oliveira; Daniel Lima Ventura (Theor. Comput. Sci., 2018)

The Computational Relevance of Formal Logic Through Formal Proofs. - Ariane Alves Almeida; Ana Cristina Rocha Oliveira; Thiago Mendonça Ferreira Ramos; Flávio L. C. de Moura; Mauricio Ayala-Rincón (FMTea, 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)