Mauricio Ayala-Rincón
According to our database1,
Mauricio Ayala-Rincón
authored at least 108 papers
between 1993 and 2019.
Collaborative distances:
Collaborative distances:
Timeline
Legend:
Book In proceedings Article PhD thesis OtherLinks
Homepage:
On csauthors.net:
Bibliography
2019
A formalisation of nominal α-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. Reasoning, 2019
A Formalisation of Nominal C-Matching through Unification with Protected Variables.
Electr. Notes Theor. Comput. Sci., 2019
Opposition-Based Memetic Algorithm and Hybrid Approach for Sorting Permutations by Reversals.
Evolutionary Computation, 2019
Formalizing the Dependency Pair Criterion for Innermost Termination.
CoRR, 2019
On Nominal Syntax and Permutation Fixed Points.
CoRR, 2019
The Computational Relevance of Formal Logic Through Formal Proofs.
Proceedings of the Formal Methods Teaching - Third International Workshop and Tutorial, 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
On the average number of reversals needed to sort signed permutations.
Discrete Applied Mathematics, 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
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. Reasoning, 2017
A Formalisation of Nominal α-equivalence with A and AC Function Symbols.
Electr. Notes Theor. Comput. Sci., 2017
A Grammar Compression Algorithm based on Induced Suffix Sorting.
CoRR, 2017
Nominal C-Unification.
CoRR, 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
Type Soundness for Path Polymorphism.
Electr. Notes Theor. Comput. Sci., 2016
A Practical Semi-External Memory Method for Approximate Pattern Matching.
Electr. Notes Theor. Comput. Sci., 2016
Completeness in PVS of a Nominal Unification Algorithm.
Electr. Notes Theor. Comput. Sci., 2016
Checking Overlaps of Nominal Rewriting Rules.
Electr. Notes Theor. Comput. Sci., 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.
Logic Journal of the IGPL, 2015
Preface.
Electr. Notes Theor. Comput. Sci., 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.
Logic Journal of the IGPL, 2014
A Compressed Suffix Tree Based Implementation With Low Peak Memory Usage.
Electr. Notes Theor. Comput. Sci., 2014
Hardware opposition-based PSO applied to mobile robot controllers.
Eng. Appl. of AI, 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. Formalized Reasoning, 2013
Sorting Permutations by Reversals through a Hybrid Genetic Algorithm based on Breakpoint Elimination and Exact Solutions for Signed Permutations.
Electr. Notes Theor. Comput. Sci., 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
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 Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi.
Electr. Notes 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. Reasoning, 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.
Logic Journal of the IGPL, 2009
A PVS Theory for Term Rewriting Systems.
Electr. Notes Theor. Comput. Sci., 2009
Preface.
Electr. Notes Theor. Comput. Sci., 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. Formalized Reasoning, 2008
Higher-Order Unification: A structural relation between Huet's method and the one based on explicit substitutions.
J. Applied Logic, 2008
Preface.
Electr. Notes Theor. Comput. Sci., 2008
Distributed approach to group control of elevator systems using fuzzy logic and FPGA implementation of dispatching algorithms.
Eng. Appl. of AI, 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 Distrib. Comput., 2007
A variant of the Ford-Johnson algorithm that is more space efficient.
Inf. Process. Lett., 2007
An exact parallel algorithm to compare very long biological sequences in clusters of workstations.
Cluster Computing, 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.
Journal of Applied Non-Classical 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 ELAN hardware specifications using the proof assistant PVS.
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. Logic, 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.
Revista Colombiana 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.
Revista Colombiana 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.
Electr. Notes Theor. Comput. Sci., 2002
Applying ELAN Strategies in Simulating Processors over Simple Architectures.
Electr. Notes Theor. Comput. Sci., 2002
Comparing Calculi of Explicit Substitutions with Eta-reduction.
Electr. Notes Theor. Comput. Sci., 2002
2001
Unification Modulo Presburger Arithmetic and Other Decidable Theories.
Revista Colombiana de Computación, 2001
Unification via the lambda se-Style of Explicit Substitutions.
Logic Journal of the 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.
Revista Colombiana de Computación, 2000
Unification via se-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
1993
Expressiveness of conditional equational systems with built-in predicates.
PhD thesis, 1993