Mauricio Ayala-Rincón

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

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

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


  Loading...