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

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 AC-Matching. - Mauricio Ayala-Rincón; Maribel Fernández; Gabriel Ferreira Silva; Temur Kutsia; Daniele Nantes-Sobrinho (CICM, 2023)

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)

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)