Mauricio Ayala-Rincón

Orcid: 0000-0003-0089-3905

According to our database1, Mauricio Ayala-Rincón authored at least 134 papers between 1993 and 2023.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2023
Formal Verification of Termination Criteria for First-Order Recursive Functions.
J. Autom. Reason., December, 2023

On the behavior of parallel island models.
Appl. Soft Comput., November, 2023

Equational Anti-Unification over Absorption Theories.
CoRR, 2023

Nominal AC-Matching.
Proceedings of the Intelligent Computer Mathematics - 16th International Conference, 2023

Formalization of Algebraic Theorems in PVS (Invited Talk).
Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

A Provably Correct Floating-Point Implementation of Well Clear Avionics Concepts.
Proceedings of the Formal Methods in Computer-Aided Design, 2023

2022
The impact of formulation of cost function in Task Mapping Problem on NoCs using bio-inspired based-metaheuristics.
Microprocess. Microsystems, October, 2022

Introduction to the special issue: Confluence.
Math. Struct. Comput. Sci., August, 2022

Grammar Compression by Induced Suffix Sorting.
ACM J. Exp. Algorithmics, 2022

Formalization of the Computational Theory of a Turing Complete Functional Language Model.
J. Autom. Reason., 2022

Reconfigurable Heterogeneous Parallel Island Models.
Proceedings of the IEEE Symposium Series on Computational Intelligence, 2022

Hall's Theorem for Enumerable Families of Finite Sets.
Proceedings of the Intelligent Computer Mathematics - 15th International Conference, 2022

A Certified Algorithm for AC-Unification.
Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, 2022

2021
Formalising nominal C-unification generalised with protected variables.
Math. Struct. Comput. Sci., 2021

Formalization of Ring Theory in PVS.
J. Autom. Reason., 2021

Heterogeneous Parallel Island Models.
Proceedings of the IEEE Symposium Series on Computational Intelligence, 2021

Nominal Equational Problems.
Proceedings of the Foundations of Software Science and Computation Structures, 2021

2020
Formalizing the dependency pair criterion for innermost termination.
Sci. Comput. Program., 2020

Introduction to the special issue: Unification.
Math. Struct. Comput. Sci., 2020

On Nominal Syntax and Permutation Fixed Points.
Log. Methods Comput. Sci., 2020

Teaching Interactive Proofs to Mathematicians.
Proceedings of the Proceedings 9th International Workshop on Theorem Proving Components for Educational Software, 2020

An Investigation into General Nominal Equational Problems (Work in progress).
Proceedings of the 34th International Workshop on Unification, 2020

Parallel Social Spider Optimization Algorithms with Island Model for the Clustering Problem.
Proceedings of the Information Management and Big Data, 2020

A Study of the Impact of Formulation of Cost Function in Task Mapping Problem on NoCs.
Proceedings of the IEEE Nordic Circuits and Systems Conference, NorCAS 2020, Oslo, 2020

Behavior of Bioinspired Algorithms in Parallel Island Models.
Proceedings of the IEEE Congress on Evolutionary Computation, 2020

2019
A formalisation of nominal <i>α</i>-equivalence with A, C, and AC function symbols.
Theor. Comput. Sci., 2019

Typed path polymorphism.
Theor. Comput. Sci., 2019

Selected Extended Papers of ITP 2017 - Preface.
J. Autom. Reason., 2019

Opposition-Based Memetic Algorithm and Hybrid Approach for Sorting Permutations by Reversals.
Evol. Comput., 2019

The Computational Relevance of Formal Logic Through Formal Proofs.
Proceedings of the Formal Methods Teaching - Third International Workshop and Tutorial, 2019

Application of an Adaptive Genetic Algorithm for Task Mapping Optimisation on a Wormhole-based Real-time Network-on-Chip.
Proceedings of the IX Brazilian Symposium on Computing Systems Engineering, 2019

On Solving Nominal Disunification Constraints.
Proceedings of the 14th Workshop on Logical and Semantic Frameworks with Applications, 2019

A Certified Functional Nominal C-Unification Algorithm.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2019

Parallel Island Model Genetic Algorithms applied in NP-Hard problems.
Proceedings of the IEEE Congress on Evolutionary Computation, 2019

2018
Nominal essential intersection types.
Theor. Comput. Sci., 2018

A Formalisation of Nominal C-Matching through Unification with Protected Variables.
Proceedings of the 13th Workshop on Logical and Semantic Frameworks with Applications, 2018

On the average number of reversals needed to sort signed permutations.
Discret. Appl. Math., 2018

Formalization of the Undecidability of the Halting Problem for a Functional Language.
Proceedings of the Logic, Language, Information, and Computation, 2018

Fixed-Point Constraints for Nominal Equational Unification.
Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, 2018

A Grammar Compression Algorithm Based on Induced Suffix Sorting.
Proceedings of the 2018 Data Compression Conference, 2018

Parallel Multi-Island Genetic Algotirth for Sorting Unsigned Genomes by Reversals.
Proceedings of the 2018 IEEE Congress on Evolutionary Computation, 2018

2017
Applied Logic for Computer Scientists - Computational Deduction and Formal Proofs
Undergraduate Topics in Computer Science, Springer, ISBN: 978-3-319-51653-0, 2017

Logical and Semantic Frameworks with Applications.
Theor. Comput. Sci., 2017

Intruder deduction problem for locally stable theories with normal forms and inverses.
Theor. Comput. Sci., 2017

Confluence of Orthogonal Term Rewriting Systems in the Prototype Verification System.
J. Autom. Reason., 2017

Nominal C-Unification.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2017

On Solving Nominal Fixpoint Equations.
Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

Variable neighborhood search for the large phylogeny problem using gene order data.
Proceedings of the 2017 IEEE Congress on Evolutionary Computation, 2017

Parallel genetic algorithms with sharing of individuals for sorting unsigned genomes by reversals.
Proceedings of the 2017 IEEE Congress on Evolutionary Computation, 2017

2016
A Formalisation of Nominal α-equivalence with A and AC Function Symbols.
Proceedings of the 11th Workshop on Logical and Semantic Frameworks with Applications, 2016

Nominal Narrowing.
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, 2016

Parallel memetic genetic algorithms for sorting unsigned genomes by translocations.
Proceedings of the IEEE Congress on Evolutionary Computation, 2016

2015
Parallelization of genetic algorithms for sorting permutations by reversals over biological data.
Int. J. Hybrid Intell. Syst., 2015

Explicit substitution calculi with de Bruijn indices and intersection type systems.
Log. J. IGPL, 2015

Type Soundness for Path Polymorphism.
Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications, 2015

A Practical Semi-External Memory Method for Approximate Pattern Matching.
Proceedings of the Third Workshop-School on Theoretical Computer Science, 2015

Completeness in PVS of a Nominal Unification Algorithm.
Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications, 2015

Checking Overlaps of Nominal Rewriting Rules.
Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications, 2015

Formalising Confluence in PVS.
Proceedings of the Eleventh International Workshop on Developments in Computational Models, 2015

Memetic and Opposition-Based Learning Genetic Algorithms for Sorting Unsigned Genomes by Translocations.
Proceedings of the Advances in Nature and Biologically Inspired Computing, 2015

Computing translocation distance by a genetic algorithm.
Proceedings of the 2015 Latin American Computing Conference, 2015

2014
First-order unification in the PVS proof assistant.
Log. J. IGPL, 2014

Preface.
Proceedings of the Ninth Workshop on Logical and Semantic Frameworks, with Applications, 2014

Hardware opposition-based PSO applied to mobile robot controllers.
Eng. Appl. Artif. Intell., 2014

Verification of Hardware Implementations through Correctness of their Recursive Definitions in PVS.
Proceedings of the 27th Symposium on Integrated Circuits and Systems Design, 2014

On the Computability of Relations on λ-Terms and Rice's Theorem - The Case of the Expansion Problem for Explicit Substitutions.
Proceedings of the LATIN 2014: Theoretical Informatics - 11th Latin American Symposium, Montevideo, Uruguay, March 31, 2014

Metaconfluence of Calculi with Explicit Substitutions at a Distance.
Proceedings of the 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, 2014

Memetic algorithm for sorting unsigned permutations by reversals.
Proceedings of the IEEE Congress on Evolutionary Computation, 2014

2013
Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model.
J. Formaliz. Reason., 2013

A Compressed Suffix Tree Based Implementation With Low Peak Memory Usage.
Proceedings of the XXXIX Latin American Computer Conference - Selected Papers, 2013

Parallelization and virtualization of genetic algorithms for sorting permutations by reversals.
Proceedings of the Fifth World Congress on Nature and Biologically Inspired Computing, 2013

Hardware-based parallel firefly algorithm for embedded applications.
Proceedings of the 2013 NASA/ESA Conference on Adaptive Hardware and Systems, 2013

2012
Sorting Permutations by Reversals through a Hybrid Genetic Algorithm based on Breakpoint Elimination and Exact Solutions for Signed Permutations.
Proceedings of the XXXVIII Latin American Computer Conference - Selected Papers, 2012

Formalizing the Confluence of Orthogonal Rewriting Systems
Proceedings of the Proceedings Seventh Workshop on Logical and Semantic Frameworks, 2012

Elementary Deduction Problem for Locally Stable Theories with Normal Forms
Proceedings of the Proceedings Seventh Workshop on Logical and Semantic Frameworks, 2012

2011
Preface.
Theor. Comput. Sci., 2011

A Formalization of the Theorem of Existence of First-Order Most General Unifiers
Proceedings of the Proceedings 6th Workshop on Logical and Semantic Frameworks with Applications, 2011

Opposition-based shuffled PSO with passive congregation applied to FM matching synthesis.
Proceedings of the IEEE Congress on Evolutionary Computation, 2011

2010
A Formalization of the Knuth-Bendix(-Huet) Critical Pair Theorem.
J. Autom. Reason., 2010

A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi.
Proceedings of the Fifth Logical and Semantic Frameworks, with Applications Workshop, 2010

Intersection Type Systems and Explicit Substitutions Calculi.
Proceedings of the Logic, 2010

Reduction of the Intruder Deduction Problem into Equational Elementary Deduction for Electronic Purse Protocols with Blind Signatures.
Proceedings of the Logic, 2010

Verification of the Completeness of Unification Algorithms à la Robinson.
Proceedings of the Logic, 2010

Hardware Particle Swarm Optimization Based on the Attractive-Repulsive Scheme for Embedded Applications.
Proceedings of the ReConFig'10: 2010 International Conference on Reconfigurable Computing and FPGAs, 2010

Comparison between two FPGA implementations of the Particle Swarm Optimization algorithm for high-performance embedded applications.
Proceedings of the Fifth International Conference on Bio-Inspired Computing: Theories and Applications, 2010

Accelerating the Shuffled Frog Leaping algorithm by parallel implementations in FPGAs.
Proceedings of the Fifth International Conference on Bio-Inspired Computing: Theories and Applications, 2010

2009
Explicit substitutions calculi with one step Eta-reduction decided explicitly.
Log. J. IGPL, 2009

Preface.
Proceedings of the Fourth Workshop on Logical and Semantic Frameworks, with Applications, 2009

Principal Typings in a Restricted Intersection Type System for Beta Normal Forms with De Bruijn Indices
Proceedings of the Proceedings Ninth International Workshop on Reduction Strategies in Rewriting and Programming, 2009

Parameterizable floating-point library for arithmetic operations in FPGAs.
Proceedings of the 22st Annual Symposium on Integrated Circuits and Systems Design: Chip on the Dunes, 2009

Hardware Architecture for Particle Swarm Optimization Using Floating-Point Arithmetic.
Proceedings of the Ninth International Conference on Intelligent Systems Design and Applications, 2009

2008
A Formalization of Newman's and Yokouchi's Lemmas in a Higher-Order Language.
J. Formaliz. Reason., 2008

Higher-Order Unification: A structural relation between Huet's method and the one based on explicit substitutions.
J. Appl. Log., 2008

A PVS Theory for Term Rewriting Systems.
Proceedings of the Third Workshop on Logical and Semantic Frameworks with Applications, 2008

Distributed approach to group control of elevator systems using fuzzy logic and FPGA implementation of dispatching algorithms.
Eng. Appl. Artif. Intell., 2008

A Theory for Abstract Reduction Systems in PVS.
CLEI Electron. J., 2008

Principal Typings for Explicit Substitutions Calculi.
Proceedings of the Logic and Theory of Algorithms, 2008

2007
Parallel strategies for the local biological sequence alignment in a cluster of workstations.
J. Parallel Distributed Comput., 2007

A variant of the Ford-Johnson algorithm that is more space efficient.
Inf. Process. Lett., 2007

Preface.
Proceedings of the Second Workshop on Logical and Semantic Frameworks, with Applications, 2007

An exact parallel algorithm to compare very long biological sequences in clusters of workstations.
Clust. Comput., 2007

Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm.
Proceedings of the Logic, 2007

2006
Prototyping time- and space-efficient computations of algebraic operations over dynamically reconfigurable systems modeled by rewriting-logic.
ACM Trans. Design Autom. Electr. Syst., 2006

SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi.
J. Appl. Non Class. Logics, 2006

Implementation of dispatching algorithms for elevator systems using reconfigurable architectures.
Proceedings of the 19th Annual Symposium on Integrated Circuits and Systems Design, 2006

SAEPTUM: verification of <i>ELAN</i> hardware specifications using the proof assistant <i>PVS</i>.
Proceedings of the 19th Annual Symposium on Integrated Circuits and Systems Design, 2006

Implementation, Simulation and Validation of Dispatching Algorithms for Elevator Systems.
Proceedings of the 2006 IEEE International Conference on Reconfigurable Computing and FPGA's, 2006

2005
Comparing and implementing calculi of explicit substitutions with eta-reduction.
Ann. Pure Appl. Log., 2005

A Modification of the Landau-Vishkin Algorithm Computing Longest Common Extensions via Suffix Arrays.
Proceedings of the Advances in Bioinformatics and Computational Biology, 2005

Parallel Smith-Waterman Algorithm for Local DNA Comparison in a Cluster of Workstations.
Proceedings of the Experimental and Efficient Algorithms, 4th InternationalWorkshop, 2005

VANNGen: a flexible CAD tool for hardware implementation of artificial neural networks.
Proceedings of the 2005 International Conference on Reconfigurable Computing and FPGAs, 2005

Parallel Strategies for Local Biological Sequence Alignment in a Cluster of Workstations.
Proceedings of the 19th International Parallel and Distributed Processing Symposium (IPDPS 2005), 2005

FELIX: Using Rewriting-Logic for Generating Functionally Equivalent Implementations.
Proceedings of the 2005 International Conference on Field Programmable Logic and Applications (FPL), 2005

2004
Reconfigurable Systems for Sequence Alignment and for General Dynamic Programming.
Proceedings of the III Brazilian Workshop on Bioinformatics, 2004

Modeling and prototyping dynamically reconfigurable systems for efficient computation of dynamic programming methods by rewriting-logic.
Proceedings of the 17th Annual Symposium on Integrated Circuits and Systems Design, 2004

Second-Order Matching via Explicit Substitutions.
Proceedings of the Logic for Programming, 2004

2003
On Automating the Extraction of Programs from Termination Proofs.
Rev. Colomb. de Computación, 2003

A Linear Time Lower Bound on McCreight and General Updating Algorithms for Suffix Trees.
Algorithmica, 2003

Efficient Computation of Algebraic Operations over Dynamically Reconfigurable Systems Specified by Rewriting-Logic Environments.
Proceedings of the 23rd International Conference of the Chilean Computer Science Society (SCCC 2003), 2003

Modeling a Reconfigurable System for Computing the FFT in Place via Rewriting-Logic.
Proceedings of the 16th Annual Symposium on Integrated Circuits and Systems Design, 2003

Using Rewriting-Logic Notation for Funcional Verification in Data-Stream Based Reconfigurable Computing.
Proceedings of the Forum on specification and Design Languages, 2003

2002
Architectural Specification, Exploration and Simulation Through Rewriting-Logic.
Rev. Colomb. de Computación, 2002

A framework to visualize equivalences between computational models of regular languages.
Inf. Process. Lett., 2002

On automating the extraction of programs from proofs using product types.
Proceedings of the 9th Workhop on Logic, Language, Information and Computation, 2002

Applying ELAN Strategies in Simulating Processors over Simple Architectures.
Proceedings of the 2nd International Workshop on Reduction Strategies in Rewriting and Programming, 2002

Comparing Calculi of Explicit Substitutions with Eta-reduction.
Proceedings of the 9th Workhop on Logic, Language, Information and Computation, 2002

2001
Unification Modulo Presburger Arithmetic and Other Decidable Theories.
Rev. Colomb. de Computación, 2001

Unification via the lambda s<sub>e</sub>-Style of Explicit Substitutions.
Log. J. IGPL, 2001

An Efficient Strategy for Word-Cycle Completion in Finitely Presented Groups.
Proceedings of the 21st International Conference of the Chilean Computer Science Society (SCCC 2001), 2001

2000
Explicit Substitions and All That.
Rev. Colomb. de Computación, 2000

Unification via <i>s<sub>e</sub></i>-style of explicit substitution.
Proceedings of the 2nd international ACM SIGPLAN conference on on Principles and practice of declarative programming, 2000

1998
A Linear Time Lower Bound on Updating Algorithms for Suffix Trees.
Proceedings of the String Processing and Information Retrieval: A South American Symposium, 1998

Church-Rosser Property for Conditional Rewriting Systems with Built-in Predicates as Premises.
Proceedings of the Frontiers of Combining Systems, Second International Workshop, 1998

1993
Expressiveness of conditional equational systems with built-in predicates.
PhD thesis, 1993


  Loading...