Expressiveness of conditional equational systems with built-in predicates. - Mauricio Ayala-Rincón (1993)

Church-Rosser Property for Conditional Rewriting Systems with Built-in Predicates as Premises. - Mauricio Ayala-Rincón (FroCoS, 1998)

A Linear Time Lower Bound on Updating Algorithms for Suffix Trees. - Mauricio Ayala-Rincón; Paulo D. Conejo (SPIRE, 1998)

Unification via se-style of explicit substitution. - Mauricio Ayala-Rincón; Fairouz Kamareddine (PPDP, 2000)

Explicit Substitions and All That. - Mauricio Ayala-Rincón; César A. Muñoz (Rev. Colomb. de Computación, 2000)

An Efficient Strategy for Word-Cycle Completion in Finitely Presented Groups. - Luiz M. R. Gadelha Jr.; Mauricio Ayala-Rincón (SCCC, 2001)

Unification via the lambda se-Style of Explicit Substitutions. - Mauricio Ayala-Rincón; Fairouz Kamareddine (Log. J. IGPL, 2001)

Unification Modulo Presburger Arithmetic and Other Decidable Theories. - Mauricio Ayala-Rincón; Ivan E. Tavares de Araújo (Rev. Colomb. de Computación, 2001)

Comparing Calculi of Explicit Substitutions with Eta-reduction. - Mauricio Ayala-Rincón; Flávio L. C. de Moura; Fairouz Kamareddine (WoLLIC, 2002)

Applying ELAN Strategies in Simulating Processors over Simple Architectures. - Mauricio Ayala-Rincón; Rinaldi Maya Neto; Ricardo P. Jacobi; Carlos H. Llanos; Reiner W. Hartenstein (WRS, 2002)

On automating the extraction of programs from proofs using product types. - Fairouz Kamareddine; François Monin; Mauricio Ayala-Rincón (WoLLIC, 2002)

A framework to visualize equivalences between computational models of regular languages. - Mauricio Ayala-Rincón; Alexsandro F. da Fonseca; Haydée Werneck Poubel; José de Siqueira (Inf. Process. Lett., 2002)

Architectural Specification, Exploration and Simulation Through Rewriting-Logic. - Mauricio Ayala-Rincón; Reiner W. Hartenstein; Rinaldi Maya Neto; Ricardo P. Jacobi; Carlos H. Llanos (Rev. Colomb. de Computación, 2002)

Using Rewriting-Logic Notation for Funcional Verification in Data-Stream Based Reconfigurable Computing. - Mauricio Ayala-Rincón; Ricardo P. Jacobi; Carlos H. Llanos; Reiner W. Hartenstein (FDL, 2003)

Modeling a Reconfigurable System for Computing the FFT in Place via Rewriting-Logic. - Mauricio Ayala-Rincón; Rodrigo Borges Nogueira; Carlos H. Llanos; Ricardo P. Jacobi; Reiner W. Hartenstein (SBCCI, 2003)

Efficient Computation of Algebraic Operations over Dynamically Reconfigurable Systems Specified by Rewriting-Logic Environments. - Mauricio Ayala-Rincón; Rodrigo Borges Nogueira; Carlos H. Llanos; Ricardo P. Jacobi; Reiner W. Hartenstein (SCCC, 2003)

A Linear Time Lower Bound on McCreight and General Updating Algorithms for Suffix Trees. - Mauricio Ayala-Rincón; Paulo D. Conejo (Algorithmica, 2003)

On Automating the Extraction of Programs from Termination Proofs. - Fairouz Kamareddine; François Monin; Mauricio Ayala-Rincón (Rev. Colomb. de Computación, 2003)

Second-Order Matching via Explicit Substitutions. - Flávio L. C. de Moura; Fairouz Kamareddine; Mauricio Ayala-Rincón (LPAR, 2004)

Modeling and prototyping dynamically reconfigurable systems for efficient computation of dynamic programming methods by rewriting-logic. - Mauricio Ayala-Rincón; Ricardo P. Jacobi; Luis Gustavo A. Carvalho; Carlos H. Llanos; Reiner W. Hartenstein (SBCCI, 2004)

Reconfigurable Systems for Sequence Alignment and for General Dynamic Programming. - Ricardo P. Jacobi; Mauricio Ayala-Rincón; Luis Gustavo A. Carvalho; Carlos H. Llanos; Reiner W. Hartenstein (WOB, 2004)

FELIX: Using Rewriting-Logic for Generating Functionally Equivalent Implementations. - Carlos Morra; Jürgen Becker 001; Mauricio Ayala-Rincón; Reiner W. Hartenstein (FPL, 2005)

Parallel Strategies for Local Biological Sequence Alignment in a Cluster of Workstations. - Azzedine Boukerche; Alba Cristina Magalhaes Alves de Melo; Mauricio Ayala-Rincón; Thomas Mailleux Santana (IPDPS, 2005)

VANNGen: a flexible CAD tool for hardware implementation of artificial neural networks. - André L. S. Braga; Carlos H. Llanos; Mauricio Ayala-Rincón; Ricardo P. Jacobi (ReConFig, 2005)

Parallel Smith-Waterman Algorithm for Local DNA Comparison in a Cluster of Workstations. - Azzedine Boukerche; Alba Cristina Magalhaes Alves de Melo; Mauricio Ayala-Rincón; Thomas Mailleux Santana (WEA, 2005)

A Modification of the Landau-Vishkin Algorithm Computing Longest Common Extensions via Suffix Arrays. - Rodrigo de Castro Miranda; Mauricio Ayala-Rincón (BSB, 2005)

Comparing and implementing calculi of explicit substitutions with eta-reduction. - Mauricio Ayala-Rincón; Flávio L. C. de Moura; Fairouz Kamareddine (Ann. Pure Appl. Log., 2005)

Implementation, Simulation and Validation of Dispatching Algorithms for Elevator Systems. - Daniel M. Muñoz; Carlos H. Llanos; Mauricio Ayala-Rincón; Rudi H. van Els (ReConFig, 2006)

SAEPTUM: verification of ELAN hardware specifications using the proof assistant PVS. - Mauricio Ayala-Rincón; Thomas Mailleux Santana (SBCCI, 2006)

Implementation of dispatching algorithms for elevator systems using reconfigurable architectures. - Daniel M. Muñoz; Carlos H. Llanos; Mauricio Ayala-Rincón; Rudi H. van Els; Renato P. Almeida (SBCCI, 2006)

SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi. - Flávio L. C. de Moura; Mauricio Ayala-Rincón; Fairouz Kamareddine (J. Appl. Non Class. Logics, 2006)

Prototyping time- and space-efficient computations of algebraic operations over dynamically reconfigurable systems modeled by rewriting-logic. - Mauricio Ayala-Rincón; Carlos H. Llanos; Ricardo P. Jacobi; Reiner W. Hartenstein (ACM Trans. Design Autom. Electr. Syst., 2006)

Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm. - André Luiz Galdino; César A. Muñoz; Mauricio Ayala-Rincón (WoLLIC, 2007)

An exact parallel algorithm to compare very long biological sequences in clusters of workstations. - Azzedine Boukerche; Alba Cristina Magalhaes Alves de Melo; Edans Flavius de Oliveira Sandes; Mauricio Ayala-Rincón (Clust. Comput., 2007)

A variant of the Ford-Johnson algorithm that is more space efficient. - Mauricio Ayala-Rincón; Bruno T. de Abreu; José de Siqueira (Inf. Process. Lett., 2007)

Parallel strategies for the local biological sequence alignment in a cluster of workstations. - Azzedine Boukerche; Alba Cristina Magalhaes Alves de Melo; Mauricio Ayala-Rincón; Maria Emília Telles Walter (J. Parallel Distributed Comput., 2007)

Principal Typings for Explicit Substitutions Calculi. - Daniel Lima Ventura; Mauricio Ayala-Rincón; Fairouz Kamareddine (CiE, 2008)

A Theory for Abstract Reduction Systems in PVS. - André Luiz Galdino; Mauricio Ayala-Rincón (CLEI Electron. J., 2008)

Distributed approach to group control of elevator systems using fuzzy logic and FPGA implementation of dispatching algorithms. - Daniel M. Muñoz; Carlos H. Llanos; Mauricio Ayala-Rincón; Rudi H. van Els (Eng. Appl. Artif. Intell., 2008)

A PVS Theory for Term Rewriting Systems. - André Luiz Galdino; Mauricio Ayala-Rincón (LSFA, 2008)

Higher-Order Unification: A structural relation between Huet's method and the one based on explicit substitutions. - Flávio L. C. de Moura; Mauricio Ayala-Rincón; Fairouz Kamareddine (J. Appl. Log., 2008)

A Formalization of Newman's and Yokouchi's Lemmas in a Higher-Order Language. - André Luiz Galdino; Mauricio Ayala-Rincón (J. Formaliz. Reason., 2008)

Hardware Architecture for Particle Swarm Optimization Using Floating-Point Arithmetic. - Daniel M. Muñoz Arboleda; Carlos H. Llanos; Leandro dos Santos Coelho; Mauricio Ayala-Rincón (ISDA, 2009)

Parameterizable floating-point library for arithmetic operations in FPGAs. - Diego F. Sánchez; Daniel M. Muñoz; Carlos H. Llanos; Mauricio Ayala-Rincón (SBCCI, 2009)

Principal Typings in a Restricted Intersection Type System for Beta Normal Forms with De Bruijn Indices - Daniel Lima Ventura; Mauricio Ayala-Rincón; Fairouz Kamareddine (WRS, 2009)

Preface. - Mauricio Ayala-Rincón; Fairouz Kamareddine (LSFA, 2009)

Preface. - Mauricio Ayala-Rincón; Edward Hermann Haeusler (Log. J. IGPL, 2009)

Explicit substitutions calculi with one step Eta-reduction decided explicitly. - Daniel Lima Ventura; Mauricio Ayala-Rincón; Fairouz Kamareddine (Log. J. IGPL, 2009)

Accelerating the Shuffled Frog Leaping algorithm by parallel implementations in FPGAs. - Daniel M. Muñoz; Carlos H. Llanos; Leandro dos Santos Coelho; Mauricio Ayala-Rincón (BIC-TA, 2010)

Comparison between two FPGA implementations of the Particle Swarm Optimization algorithm for high-performance embedded applications. - Daniel M. Muñoz; Carlos H. Llanos; Leandro dos Santos Coelho; Mauricio Ayala-Rincón (BIC-TA, 2010)

Hardware Particle Swarm Optimization Based on the Attractive-Repulsive Scheme for Embedded Applications. - Daniel M. Muñoz; Carlos H. Llanos; Leandro dos Santos Coelho; Mauricio Ayala-Rincón (ReConFig, 2010)

Verification of the Completeness of Unification Algorithms à la Robinson. - Andréia B. Avelar; Flávio L. C. de Moura; André Luiz Galdino; Mauricio Ayala-Rincón (WoLLIC, 2010)

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)

Intersection Type Systems and Explicit Substitutions Calculi. - Daniel Lima Ventura; Mauricio Ayala-Rincón; Fairouz Kamareddine (WoLLIC, 2010)

A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi. - Flávio L. C. de Moura; A. V. Barbosa; Mauricio Ayala-Rincón; Fairouz Kamareddine (LSFA, 2010)

A Formalization of the Knuth-Bendix(-Huet) Critical Pair Theorem. - André Luiz Galdino; Mauricio Ayala-Rincón (J. Autom. Reason., 2010)

Opposition-based shuffled PSO with passive congregation applied to FM matching synthesis. - Daniel M. Muñoz; Carlos H. Llanos; Leandro dos Santos Coelho; Mauricio Ayala-Rincón (IEEE Congress on Evolutionary Computation, 2011)

A Formalization of the Theorem of Existence of First-Order Most General Unifiers - Andréia B. Avelar; André Luiz Galdino; Flávio L. C. de Moura; Mauricio Ayala-Rincón (LSFA, 2011)

Preface. - Mauricio Ayala-Rincón; Elaine Pimentel; Fairouz Kamareddine (Theor. Comput. Sci., 2011)

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

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

Sorting Permutations by Reversals through a Hybrid Genetic Algorithm based on Breakpoint Elimination and Exact Solutions for Signed Permutations. - José Luis Soncco-Álvarez; Mauricio Ayala-Rincón (CLEI Selected Papers, 2012)

Hardware-based parallel firefly algorithm for embedded applications. - Daniel M. Muñoz; Carlos H. Llanos; Leandro dos Santos Coelho; Mauricio Ayala-Rincón (AHS, 2013)

Parallelization and virtualization of genetic algorithms for sorting permutations by reversals. - José Luis Soncco-Álvarez; Gabriel Marchesan Almeida; Jürgen Becker 001; Mauricio Ayala-Rincón (NaBIC, 2013)

A Compressed Suffix Tree Based Implementation With Low Peak Memory Usage. - Daniel Saad Nogueira Nunes; Mauricio Ayala-Rincón (CLEI Selected Papers, 2013)

Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model. - Mauricio Ayala-Rincón; Yuri Santos Rego (J. Formaliz. Reason., 2013)

Memetic algorithm for sorting unsigned permutations by reversals. - José Luis Soncco-Álvarez; Mauricio Ayala-Rincón (IEEE Congress on Evolutionary Computation, 2014)

Metaconfluence of Calculi with Explicit Substitutions at a Distance. - Flávio L. C. de Moura; Delia Kesner; Mauricio Ayala-Rincón (FSTTCS, 2014)

On the Computability of Relations on λ-Terms and Rice's Theorem - The Case of the Expansion Problem for Explicit Substitutions. - Edward Hermann Haeusler; Mauricio Ayala-Rincón (LATIN, 2014)

Verification of Hardware Implementations through Correctness of their Recursive Definitions in PVS. - Ariane Alves Almeida; Carlos H. Llanos; Janier Arias-Garcia; Mauricio Ayala-Rincón (SBCCI, 2014)

Hardware opposition-based PSO applied to mobile robot controllers. - Daniel M. Muñoz; Carlos H. Llanos; Leandro dos Santos Coelho; Mauricio Ayala-Rincón (Eng. Appl. Artif. Intell., 2014)

Preface. - Mauricio Ayala-Rincón; Ian Mackie (LSFA, 2014)

First-order unification in the PVS proof assistant. - Andréia Borges Avelar; André Luiz Galdino; Flávio Leonardo Cavalcanti de Moura; Mauricio Ayala-Rincón (Log. J. IGPL, 2014)

Computing translocation distance by a genetic algorithm. - Lucas A. da Silveira; José Luis Soncco-Álvarez; Thaynara A. de Lima; Mauricio Ayala-Rincón (CLEI, 2015)

Memetic and Opposition-Based Learning Genetic Algorithms for Sorting Unsigned Genomes by Translocations. - Lucas A. da Silveira; José Luis Soncco-Álvarez; Thaynara A. de Lima; Mauricio Ayala-Rincón (NaBIC, 2015)

Formalising Confluence in PVS. - Mauricio Ayala-Rincón (DCM, 2015)

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)

A Practical Semi-External Memory Method for Approximate Pattern Matching. - Daniel Saad Nogueira Nunes; Mauricio Ayala-Rincón (WEIT, 2015)

Type Soundness for Path Polymorphism. - Andrés Viso; Eduardo Bonelli; Mauricio Ayala-Rincón (LSFA, 2015)

Explicit substitution calculi with de Bruijn indices and intersection type systems. - Daniel Lima Ventura; Fairouz Kamareddine; Mauricio Ayala-Rincón (Log. J. IGPL, 2015)

Parallelization of genetic algorithms for sorting permutations by reversals over biological data. - José Luis Soncco-Álvarez; Gabriel Marchesan Almeida; Jürgen Becker 001; Mauricio Ayala-Rincón (Int. J. Hybrid Intell. Syst., 2015)

Parallel memetic genetic algorithms for sorting unsigned genomes by translocations. - Lucas A. da Silveira; José Luis Soncco-Álvarez; Mauricio Ayala-Rincón (CEC, 2016)

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)

Parallel genetic algorithms with sharing of individuals for sorting unsigned genomes by reversals. - Lucas Angelo da Silveira; José Luis Soncco-Álvarez; Mauricio Ayala-Rincón (CEC, 2017)

Variable neighborhood search for the large phylogeny problem using gene order data. - José Luis Soncco-Álvarez; Mauricio Ayala-Rincón (CEC, 2017)

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)

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)

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)

Logical and Semantic Frameworks with Applications. - Mauricio Ayala-Rincón; Ian Mackie; Ugo Montanari (Theor. Comput. Sci., 2017)

Applied Logic for Computer Scientists - Computational Deduction and Formal Proofs - Mauricio Ayala-Rincón; Flávio L. C. de Moura (Springer, 2017)

Parallel Multi-Island Genetic Algotirth for Sorting Unsigned Genomes by Reversals. - Lucas A. da Silveira; José Luis Soncco-Álvarez; Thaynara A. de Lima; Mauricio Ayala-Rincón (CEC, 2018)

A Grammar Compression Algorithm Based on Induced Suffix Sorting. - Daniel Saad Nogueira Nunes; Felipe A. Louza; Simon Gog; Mauricio Ayala-Rincón; Gonzalo Navarro 001 (DCC, 2018)

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

Formalization of the Undecidability of the Halting Problem for a Functional Language. - Thiago Mendonça Ferreira Ramos; César A. Muñoz; Mauricio Ayala-Rincón; Mariano M. Moscato; Aaron Dutle; Anthony Narkawicz (WoLLIC, 2018)

On the average number of reversals needed to sort signed permutations. - Thaynara A. de Lima; Mauricio Ayala-Rincón (Discret. Appl. Math., 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)

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

Parallel Island Model Genetic Algorithms applied in NP-Hard problems. - Lucas A. da Silveira; José Luis Soncco-Álvarez; Thaynara A. de Lima; Mauricio Ayala-Rincón (CEC, 2019)

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)

Application of an Adaptive Genetic Algorithm for Task Mapping Optimisation on a Wormhole-based Real-time Network-on-Chip. - Jessé Barreto de Barros; Mauricio Ayala-Rincón; Carlos Humberto Llanos Quintero (SBESC, 2019)

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)

Opposition-Based Memetic Algorithm and Hybrid Approach for Sorting Permutations by Reversals. - José Luis Soncco-Álvarez; Daniel M. Muñoz; Mauricio Ayala-Rincón (Evol. Comput., 2019)

Selected Extended Papers of ITP 2017 - Preface. - Mauricio Ayala-Rincón; César A. Muñoz (J. Autom. Reason., 2019)

Typed path polymorphism. - Mauricio Ayala-Rincón; Eduardo Bonelli; Juan Edi; Andrés Viso (Theor. Comput. Sci., 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)

Behavior of Bioinspired Algorithms in Parallel Island Models. - Lucas A. da Silveira; José Luis Soncco-Álvarez; Thaynara A. de Lima; Mauricio Ayala-Rincón (CEC, 2020)

A Study of the Impact of Formulation of Cost Function in Task Mapping Problem on NoCs. - Jessé Barreto de Barros; Nidhi Anantharajaiah; Mauricio Ayala-Rincón; Carlos Humberto Llanos Quintero; Jürgen Becker 001 (NorCAS, 2020)

Parallel Social Spider Optimization Algorithms with Island Model for the Clustering Problem. - Edwin Alvarez-Mamani; Lauro Enciso-Rodas; Mauricio Ayala-Rincón; José Luis Soncco-Álvarez (SIMBig, 2020)

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

Teaching Interactive Proofs to Mathematicians. - Mauricio Ayala-Rincón; Thaynara Arielly de Lima (ThEdu@IJCAR, 2020)

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

Introduction to the special issue: Unification. - Mauricio Ayala-Rincón; Philippe Balbiani (Math. Struct. Comput. Sci., 2020)

Formalizing the dependency pair criterion for innermost termination. - Ariane Alves Almeida; Mauricio Ayala-Rincón (Sci. Comput. Program., 2020)

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

Heterogeneous Parallel Island Models. - Lucas A. da Silveira; José Luis Soncco-Álvarez; Thaynara A. de Lima; Mauricio Ayala-Rincón (SSCI, 2021)

Formalization of Ring Theory in PVS. - Thaynara Arielly de Lima; André Luiz Galdino; Andréia Borges Avelar; Mauricio Ayala-Rincón (J. Autom. Reason., 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)

Hall's Theorem for Enumerable Families of Finite Sets. - Fabián Fernando Serrano Suárez; Mauricio Ayala-Rincón; Thaynara Arielly de Lima (CICM, 2022)

Reconfigurable Heterogeneous Parallel Island Models. - Lucas A. da Silveira; Thaynara A. de Lima; Mauricio Ayala-Rincón (SSCI, 2022)

Formalization of the Computational Theory of a Turing Complete Functional Language Model. - Thiago Mendonça Ferreira Ramos; Ariane Alves Almeida; Mauricio Ayala-Rincón (J. Autom. Reason., 2022)

Grammar Compression by Induced Suffix Sorting. - Daniel Saad Nogueira Nunes; Felipe A. Louza; Simon Gog; Mauricio Ayala-Rincón; Gonzalo Navarro 001 (ACM J. Exp. Algorithmics, 2022)

Introduction to the special issue: Confluence. - Mauricio Ayala-Rincón; Samuel Mimram (Math. Struct. Comput. Sci., 2022)

The impact of formulation of cost function in Task Mapping Problem on NoCs using bio-inspired based-metaheuristics. - Jessé Barreto de Barros; Nidhi Anantharajaiah; Mauricio Ayala-Rincón; Carlos Humberto Llanos Quintero; Jürgen Becker 001 (Microprocess. Microsystems, 2022)

A Provably Correct Floating-Point Implementation of Well Clear Avionics Concepts. - Nikson Bernardes Fernandes Ferreira; Mariano M. Moscato; Laura Titolo; Mauricio Ayala-Rincón (FMCAD, 2023)

Formalization of Algebraic Theorems in PVS (Invited Talk). - Mauricio Ayala-Rincón; Thaynara Arielly de Lima; Andréia B. Avelar; André Luiz Galdino (LPAR, 2023)

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

Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms. - Thaynara Arielly de Lima; Andréia Borges Avelar; André Luiz Galdino; Mauricio Ayala-Rincón (LSFA/HCVS, 2023)

On the behavior of parallel island models. - Lucas A. da Silveira; Thaynara A. de Lima; Jessé Barreto de Barros; José Luis Soncco-Álvarez; Carlos H. Llanos; Mauricio Ayala-Rincón (Appl. Soft Comput., 2023)

Formal Verification of Termination Criteria for First-Order Recursive Functions. - César A. Muñoz; Mauricio Ayala-Rincón; Mariano M. Moscato; Aaron Dutle; Anthony J. Narkawicz; Ariane Alves Almeida; Andréia B. Avelar da Silva; Thiago Mendonça Ferreira Ramos (J. Autom. Reason., 2023)

Equational Anti-unification over Absorption Theories. - Mauricio Ayala-Rincón; David M. Cerna; Andres Felipe Gonzalez Barragan; Temur Kutsia (IJCAR (2), 2024)

A Formalization of the General Theory of Quaternions. - Thaynara Arielly de Lima; André Luiz Galdino; Bruno Berto de Oliveira Ribeiro; Mauricio Ayala-Rincón (ITP, 2024)

Compactness Theorem for Propositional Logic and Combinatorial Applications. - Fabián Fernando Serrano Suárez; Thaynara Arielly de Lima; Mauricio Ayala-Rincón (Arch. Formal Proofs, 2024)

On reconfiguring heterogeneous parallel island models. - Lucas A. da Silveira; Thaynara A. de Lima; Mauricio Ayala-Rincón (Swarm Evol. Comput., 2024)

Nominal Equational Rewriting and Narrowing. - Mauricio Ayala-Rincón; Maribel Fernández; Daniele Nantes-Sobrinho; Daniella Santaguida (LSFA, 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)

Combining Generalization Algorithms in Regular Collapse-Free Theories. - Mauricio Ayala-Rincón; David M. Cerna; Temur Kutsia; Christophe Ringeissen (FSCD, 2025)

Verification of an Anti-unification Algorithm in PVS. - Mauricio Ayala-Rincón; Thaynara Arielly de Lima; Maria Júlia Dias Lima; Mariano M. Moscato; Temur Kutsia (NFM, 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)

Graded Quantitative Narrowing. - Mauricio Ayala-Rincón; Thaynara Arielly de Lima; Georg Ehling; Temur Kutsia (CoRR, 2025)