Reports and Publications M. AyalaRincón
Work in progress
 L.A. da Silveira, J.L. SonccoÁlvarez and M. AyalaRincón Parallel Memetic Genetic Algorithms for Sorting
Unsigned Genomes by Translocations.
PDF, C code. Submitted, Jan. 2016.
 T.A. de Lima and M. AyalaRincón NPCompleteness of Sorting Unsigned Permutations by Reversals .
Note MAT/UnB pdf, Brasília, 2013.
 D. Nantes Sobrinho, M. Fernández and M. AyalaRincón A Proof of Polynomiality of the Elementary Deduction Problem for Electronic Purse Protocols with Blind Signatures, PDF. In preparation, 2011.
 R. de C. Miranda, M. AyalaRincón and Leon Solon, Modifications of the LandauVishkin Algorithm Computing Longest Common Extensions via Suffix Arrays and Efficient RMQ computations, (pdf). In preparation 2008.
 F.L.C. de Moura, F. Kamareddine and M. AyalaRincón Second and ThirdOrder Matching via Explicit Substitutions, (postscript, PDF). In preparation, 2006.
 M. AyalaRincón and V.A. Fernandes and A.L. Galdino, Geometrical Specification using Dependent Types in PVS, (pdf, postscript). In preparation, 2005.
 M. AyalaRincón, R. Hartenstein, R. P. Jacobi and C. Llanos, Designing Arithmetic Digital Circuits via RewritingLogic, (Postscript, 370 KB). In preparation, 2004.
 M. AyalaRincón, H. W. Poubel and R. B. Nogueira Visualizing Relations Between Computational Models and Grammars of ContextFree Languages, (ps, 250 KB; PDF, 250 KB). In preparation, 2004.
Editorial work: Proceedings and Special Issues
 Mauricio AyalaRincón, Ian Mackie: Proceeding 9th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2014). Electr. Notes Theor. Comput. Sci. vol. 312, 2015.
Contents
 Mauricio AyalaRincón, Eduardo Bonelli, Ian Mackie: Proc. 9th International Workshop on Developments in Computational Models (DCM 2013). EPTCS vol. 144, 2014.
Contents
 Mauricio AyalaRincón, Elaine Pimentel, Fairouz Kamareddine: Special Issue of Logical and Semantic Frameworks with Applications (LSFA 2008 and 2009). Theor. Comput. Sci. vol. 412(37), 2011.
Contents
 Mauricio AyalaRincón, Fairouz Kamareddine: Proc. of the Fourth Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2009). Electr. Notes Theor. Comput. Sci. vol. 256, 2009.
Contents
 Mauricio AyalaRincón, Edward Hermann Haeusler: Special Issue of Logical and Semantic Frameworks, with Applications (LSFA 2007). Logic Journal of the IGPL vol. 17(5): 487488, 2009.
Contents
 Mauricio AyalaRincón, Edward Hermann Haeusler: Proc. of the Second Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2007). Electr. Notes Theor. Comput. Sci. vol. 205, 2008.
Contents
Publications by year

2016

2015
 M. AyalaRincón, Invited Talk Formalising Confluence given in
the 11^{th} Developments in Computational Models  DCM 2015 (satellite of the 12^{th} Int. Coll. on Theoretical Aspects of Computing ICTAC 2015), Cali, Colombia, 28 October 2015.
 L.A. da Silveira, J.L. SonccoÁlvarez, T.A. de Lima and M. AyalaRincón Memetic and OppositionBased Learning Genetic Algorithms for Sorting Unsigned Genomes by Translocations.
PDF, C code, Proc. NaBIC 2015 (Vol.419, series Advances in Intelligent Systems and Computing pp 7385, 2016). Doi.
 L.A. da Silveira, J.L. SonccoÁlvarez, T.A. de Lima and M. AyalaRincón Computing Translocation Distance by a Genetic Algorithm.
PDF, C code, IEEE Xplore Proceedings CLEI 2015. Doi.
 M. AyalaRincón, Tutorial on Formal Reasoning with PVS given in
the Nat@logic Reasoning School 2015,
Natal, Brazil, 31 August  1 September 2015.
 A. Viso, E. Bonelli and M. AyalaRincón, Type Soundness for Path Polymorphism. Preproceedings LSFA 2015:318, 2015,
extended 49 page report
 M. AyalaRincón, M. Fernández and A.C. RochaOliveira, Completeness in PVS of a Nominal Unification Algorithm. Preproceedings LSFA 2015:1934, 2015.
 A.C. RochaOliveira, M. AyalaRincón and M. Fernández Formalising the Completeness of a Nominal Unification Algorithm. Ext. abstract presented in UNIF 2015 (RDP). Inf. Proc. 29^{th} Int. Workshop on Unification, pp:2732, 2015.
 M. AyalaRincón, M. Fernández, M.J. Gabbay and A.C. RochaOliveira Checking Overlaps of Nominal Rewriting Rules. Preproceedings LSFA 2015:1992014, 2015.
 D. L. Ventura, F. Kamareddine and M. AyalaRincón, Explicit substitution calculi with de Bruijn indices and intersection type systems. Logic Journal of the IGPL 23(2): 295340, 2015. Doi.
 J.L. SonccoÁlvarez, G.M. Almeida, J. Becker and M. AyalaRincón, Parallelization of genetic algorithms for sorting permutations by reversals over biological data. Int. J. Hybrid Intell. Syst. 12(1): 5364, 2015. Doi.

2014
 F.L.C. de Moura, D. Kesner and M. AyalaRincón Metaconfluence of Calculi with Explicit Substitutions at a Distance, to appear in Proc. FST&TCS 2015.
 M. AyalaRincón, Tutorial on Fomalization of Rewriting in PVS given in
the 7^{th} International School on Rewriting  ISR 2014,
Valparaíso Chile, 25 to 29 August 2014.
 A.B. Avelar, A.L. Galdino, F.L.C. de Moura and M. AyalaRincón, Firstorder unification in the PVS proof assistant, Logic Journal of the IGPL 22(5):758789, 2014. Doi.
 D. Saad and M. AyalaRincón A compressed suffix tree based implementation with low peak memory usage. ENTCS 302:7394, 2014. Doi.
 E. H. Haeusler, M. AyalaRincón, On the Computability of Relations on λTerms and Rice's Theorem  The Case of the Expansion Problem for Explicit Substitutions. LATIN 2014: LNCS, vol. 8392, pages 202213. Doi.
 D. M. Muñoz, C. H. Llanos, L. dos Santos Coelho, M. AyalaRincón, Hardware oppositionbased PSO applied to mobile robot controllers.
Engineering Applications of Artificial Intelligence 28:6477, 2014. Doi
 A.A. Almeida, J. AriasGarcia, C. H. Llanos and M. AyalaRincón, Verification of Hardware Implementations through Correctness of Their Recursive Definitions in PVS. ACM Proceedings 27th SBCCI, 2014.
 J. L. SonccoAlvarez and M. AyalaRincón, Memetic Algorithm for Sorting Unsigned Permutations by Reversals. Proceedings 2014 IEEE Congress on Evolutionary Computation (IEEE CEC 2014), 2014. Doi

2013
 F.L.C. de Moura, M. AyalaRincón, Computational Deduction and Formal Proofs Logic for Computation that is truly Computational. In Proc. 8th Colombian Conference on Computation (Tutorial) 8CCC, Armenia, Colombia, Eds. C.Collazos and W. Giraldo, U. del Quindío and U. del Cauca, pages 166174, 2013.
 Y.S. Rego and M. AyalaRincón Formalization in PVS of Balancing Properties Necessary for the Security of the DolevYao Cascade Protocol Model, Full PVS Theory:
version PVS 5.n,
version PVS 6.0).
Journal of Formalized Reasoning, 6(1):3161, 2013.
 J.L. SonccoÁlvarez, G.M. Almeida, J. Becker and M. AyalaRincón Parallelization and Virtualization of Genetic Algorithms for Sorting Permutations by Reversals. In IEEE Xplore Proc. ( 5th World Congress on Nature and Biologically Inspired Computing NaBiC ), Doi, 2013 Fargo, North Dakota, USA.
 D. Saad and M. AyalaRincón A compressed suffix tree based implementation with low peak memory usage. Accepted for publication in ENTCS CLEI 2013 (Symp. of Theory of Computation), Naiguatá, Venezuela.
 T.A. de Lima and M. AyalaRincón On the average reversal distance to sort signed permutations .
Extended abstract presented at Permutation Patterns 2013, Paris.
 A.C. Rocha Oliveira, A.L. Galdino and M. AyalaRincón Synchronizing Applications of the Parallel Moves Lemma to Formalize Confluence of Orthogonal TRSs in PVS. In Proc. Int. Workshop on Confluence, (IWC 2013, (Proc. edited by Nao Hirokawa & Vincent van Oostrom pp 4752, PVS tgz file), Eindhoven, Netherlands.
 D.M. MuñozArboleda, C. H. Llanos, L. Coelho and M. AyalaRincón, Hardwarebased Parallel Firefly Algorithm for Embedded Applications, In IEEE Proc NASA/ESA Conference on Adaptive Hardware and Systems, Doi, 2013. Torino, Italy.
 J. AriasGarcía, A. Braga, C.H. Llanos, M. AyalaRincó, R.P. Jacobi, A. Foltran, FPGA HIL Simulation of a Linear System Block for Strongly Coupled System Applications, In IEEE Xplore Proc. IEEE International Conference on Industrial Technology (ICIT). Doi, 2013, Cape Town, South Africa.

2012
 D.M. MuñozArboleda, C. H. Llanos, L. Coelho and M. AyalaRincón, Accelerating the Artificial Bee Colony Algorithm by Hardware Parallel Implementations. In 3^{rd} IEEE LA Symp. on Circuits and Systems (LASCAS 2012). (Doi)
 J. AriasGarcia, C. H. Llanos, M. AyalaRincón and R. P. Jacobi A fast and low cost architecture developed in FPGAs for solving systems of linear equations. In 3^{rd} IEEE LA Symp. on Circuits and Systems (LASCAS 2012). (Doi)
 J. AriasGarcia, C. H. Llanos, M. AyalaRincón and R. P. Jacobi , FPGA implementation of largescale Matrix Inversion using single, double and custom floatingpoint precision. In: VIII Southern Conference on Programmable Logic SPL 2012, 2012, IEEE Proc. SPL 2012, 2012. p. 16. (Doi)
 M. AyalaRincón Reusing Formal Proofs Through Isomorophisms. Invited Talk LACREST 2012 (PDFs abstract Proc. LACREST 2012 talk ).
 D. Saad and M. AyalaRincón A Compressed suffix array based index with succinct longest common prefix information. Short version accepted BSB 2012.
 A.C. Rocha Oliveira and M. AyalaRincón Formalizing the Confluence of Orthogonal Rewriting Systems. Presented in LSFA 2012. EPTCS Vol. 113:145152, 2013 (Doi, Extended Version, PVS tgz file)
 D. Nantes Sobrinho, M. Fernández and M. AyalaRincón Elementary Deduction Problem for Locally Stable Theories with Normal Forms, PDF. Presented in LSFA 2012. EPTCS Vol. 113:4560, 2013 (Doi)
 J.L. SonccoÁlvarez and M. AyalaRincón Sorting Permutations by Reversals through a Hybrid Genetic Algorithm based on Breakpoint Elimination and Exact Solutions for Signed Permutations, PDF. Special Issue best papers CLEI 2012, ENTCS Vol. 292:119133, 2013 (Doi)
.
 T.A. de Lima and M. AyalaRincón Complexity of Reversal Distance and other General Metrics on Permutation Groups, PDF.
7CCC 2012. (Doi)
 J.L. SonccoÁlvarez and M. AyalaRincón A Genetic Approach with a Simple Fitness Function for Sorting Unsigned Permutations by Reversals, Code, PDF.
7CCC 2012. (Doi)

2011
 A.B. Avelar, F.L.C. de Moura, M. AyalaRincón, and A.L. Galdino A Formalization of the Theorem of Existence of FirstOrder Most General Unifiers, PDF. In Proc. Logical and Semantic Frameworks with Applications 2011.
 D.L. Ventura, M. AyalaRincón and F. Kamareddine, Towards a characterisation of termination for explicit substitution calculi with de Bruijn indices. Presented at EBL 2011
 A.C. Rocha Oliveira and M. AyalaRincón , On the Formalization of the Property of Consequence of Orthogonal Term Rewriting SystemJ. Presented at EBL 2011
 Y.S. Rêgo and M. AyalaRincón ,Formalização em PVS de Propriedades de Balanceamento para o Modelo de Protocolos em Cascata de DolevYao . Presented at EBL 2011
 D.M. MuñozArboleda, C. H. Llanos, L. Coelho and M. AyalaRincón, Oppositionbased Shuffled PSO with Passive Congregation Applied to FM Matching Synthesis
. In Proc. IEEE Congress on Evolutionary Computation (CEC 2011) (Doi)
 D.M. MuñozArboleda, C. H. Llanos, L. Coelho and M. AyalaRincón, Hardware Particle Swarm Optimization with Passive Congregation for Embedded Applications. In Proc. 2011 VII Southern Conference on Programmable Logic (SPL) (Doi)
 J. AriasGarcia, R. P. Jacobi, C. H. Llanos and M. AyalaRincón, A Suitable FPGA Implementation of FloatingPoint Matrix Inversion based on GaussJordan Elimination. In Proc. 2011 VII Southern Conference on Programmable Logic (SPL) (Doi)
 F.L.C. de Moura, A.B. Barbosa and M. AyalaRincón A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi, (LSFA 2010) ENTCS 269:4154, 2011 (Doi)

2010
 A.L. Galdino and M. AyalaRincón A Formalization of the KnutBendix(Huet) Critical Pair Theorem
(Doi,
PVS files: TRS.tgz). J. of Automated Reasonning 45:301325, 2010.
 D.M. MuñozArboleda, D. F. Sanchez, C. H. Llanos and M. AyalaRincón, FPGA Based Floatingpoint Library for CORDIC Algorithms. In Proc. IEEE  SPL  VI Southern Programmable Logic Conference SPL 2010 Doi or Doi, pp 5560, 2010.
 D.N. Sobrino and M. AyalaRincón, Reduction of the Intruder Deduction Problem into Equational Elementary Deduction for Electronic Purse Protocols with Blind Signatures, PDF, Doi. Proc. 17th WoLLIC, LNCS vol. 6188, pag. 218231, 2010.
 A.B. Avelar, F.L.C. de Moura, M. AyalaRincón, and A.L. Galdino Verification of the Completeness of Unification Algoritms à la Robinson, PDF, Doi. Proc. 17th WoLLIC, LNCS vol. 6188, pag. 110124, 2010.
 D.L. Ventura, M. AyalaRincón and F. Kamareddine, Intersection type systems and explicit substitutions calculi , Doi Proc. 17th WoLLIC, LNCS vol. 6188, pag. 232246, 2010.
 R. B. Nogueira, A.C.A. Nascimento, F.L.C. de Moura and M. AyalaRincón, Formalization of Security Proofs Using PVS in the DolevYao Model, (PDF, PVS files: verifD_Y.tgz)). Booklet Proc. Computability in Europe CiE, 2010.
 D.M. MuñozArboleda, C. H. Llanos, L. Coelho and M. AyalaRincón, Accelerating the Shuffled Frog Leaping algorithm by parallel implementations in FPGAs. In Proc. IEEE Fifth International Conference on BioInspired Computing: Theories and Applications (BICTA 2010) Doi, pp 152634, 2010.
 D.M. MuñozArboleda, C. H. Llanos, L. Coelho and M. AyalaRincón, Comparison between two FPGA implementations of the Particle Swarm Optimization algorithm for highperformance embedded applications. In Proc. IEEE Fifth International Conference on BioInspired Computing: Theories and Applications (BICTA 2010) Doi, pp 163745, 2010.
 D.M. MuñozArboleda, D. F. Sanchez, C. H. Llanos and M. AyalaRincón, Tradeof of FPGA Design of a Floatingpoint Library for Arithmetic Operators. JICS Journal of Integrated Circuits and Systems 5:4252, 2010.

2009
 D.M. MuñozArboleda, C. H. Llanos, L. S. Coelho and M. AyalaRincón, Hardware Architecture for Particle Swarm Optimization using FloatingPoint Arithmetic. In Proc. 9th Int. Conf. on Intelligent Systems Design and Applications ISDA'09
 D.L. Ventura, M. AyalaRincón and F. Kamareddine, Principal Typings in a Restricted Intersection Type System for Beta Normal Forms with de Bruijn Indices, (Doi). In proc. 9th Int. Workshop on Rewriting Strategies  WRS'09, 2009. Published as EPTCS Vol 15:6982, 2010.
 D.L. Ventura, M. AyalaRincón and F. Kamareddine, Explicit Substitution Calculi with One Step Etareduction Decided Explicitly, (Doi). In The Logical Journal of the IGPL, vol 17(6):697718, 2009.
 D. F. Sanchez, D.M. MuñozArboleda, C. H. Llanos and M. AyalaRincón, Parameterizable Floatingpoint Library for Arithmetic Operations in FPGAs.
In Proc. 22nd Symposium on Integrated Circuits and System Design  SBCCI 09, 2009.
 D.M. MuñozArboleda, D. F. Sanchez, C. H. Llanos and M. AyalaRincón, Tradeoffs of FPGA design of floatingpoint transcendental functions. In Proc. The 17th IFIP/IEEE International Conference on Very Large Scale Integration  VLSISOC 2009
.
 D.L. Ventura, M. AyalaRincón and F. Kamareddine, Intersection Type System with de Bruijn Indices, (PDF). Presented at XV EBL/XIV SLALM, 2008; revised version published as chapter in the volume 21 "The Many Sides of Logic" of the "Studies in Logic" Series, College Publications, (M. Coniglio, W. Carnielli, I. D'Ottaviano, eds.,) 2009.

2008
 A.L. Galdino and M. AyalaRincón A Formalization of Newman's and Yokouchi Lemmas in a HigherOrder Language
Journal of Formalized Reasoning, 1(1):3950, 2008.
 A.L. Galdino and M. AyalaRincón A Theory for Abstract Reduction Systems in PVS,
CLEI electronic journal 11(2), Paper 4, 12 pages, Special Issue of Best Papers presented at CLEI'07, San José, 2008.
 D.M. MuñozArboleda, C. H. Llanos, M. AyalaRincón and R.H. van Els, Distributed approach to group control of elevator systems using fuzzy logic and FPGA implementation of dispatching algorithms. Engineering Applications of Artificial Intelligence 21(8):13091320, 2008. Doi
 D.M. MuñozArboleda, C. H. Llanos, M. AyalaRincón and R.H. van Els, FPGA Implementation of Dispatching Algorithms for Local Control of Elevator Systems. In IEEE Proc. IEEE Int. Symp. on Industrial Electronics (ISIE), (abstract, pdf, Doi), 2008.
 A.L. Galdino and M. AyalaRincón A PVS theory for Term Rewriting Systems
(PDF file,
PVS files: TRS.tgz). Presented in and to appear in ENTCS Prod. Third Logical and Semantic Frameworks, with Applications  LSFA'08, 2008.
 A.L. Galdino and M. AyalaRincón Verification of Newman's and Yokouchi Lemmas in PVS
(PDF file,
PVS files: ARS.tgz). Presentation at Computability in Europe (CiE 2008), 2008.
 D.L. Ventura, M. AyalaRincón and F. Kamareddine, Principal Typing for Explicit Substitutions Calculi, (PDF, Doi). Proc. Logic and Theory of Algorithms, 4th Conference on Computability in Europe (CiE 2008), LNCS, Vol. 5028, pages 548558, 2008.
 D.L. Ventura, M. AyalaRincón and F. Kamareddine, Intersection Type System with de Bruijn Indices, (PDF). Presentation at XV EBL/XIV SLALM, 2008. Revised version accepted for publication in the volume "The Many Sides of Logic" to be published in "Studies in Logic" Series, College
Publications, London, in 2009.
 F.L.C. de Moura, M. AyalaRincón and F. Kamareddine, HigherOrder Unification: a structural relation between Huet's method and the one based on explicit substitutions,
Journal of Applied Logic 6(1):72108, 2008.

2007
 A.L. Galdino and M. AyalaRincón A PVS theory for abstract rewriting systems
(Description: ARS.pdf,
PVS files: ARS.tgz).
In Proc. XXXIII Conferencia Latinoamericana de Informática  CLEI'07, 2007.
 A.L. Galdino, C. Muñoz and M. AyalaRincón Formal Verification of an Optimal Air Traffic Conflict Detection and Recovery Algorithm, (pdf, PVS files: kb2d.tgz). In Proc. WoLLIC 2007, SpringerVerlag LNCS Vol. 4576, pages 177188, 2007.
 D.L. Ventura, M. AyalaRincón and F. Kamareddine, Principal Typing for Explicit Substitutions Calculi, (PDF). Extended version of work in Proc. 4th Int. Workshop on HigherOrder Rewriting  HOR 2007, Ralph Mattes (Ed.), pages 4559, 2007.
 A. Boukerche, A.C.M.A. de Melo, E. Sandes and M. AyalaRincón, An Exact Parallel Algorithm to Compare Very Long Biological Sequences in Clusters of Workstations. J. Cluster Computing 10:187202, Springer 2007.
 M. AyalaRincón and B. T. de Abreu and J. de Siqueira, A Variant of the FordJohnson Algorithm that is more Space Efficient,
Information Processing Letters 102(5):201207, Elsevier 2007.
 A. Boukerche, A.C.M.A. de Melo, M. AyalaRincón and M.E.M.T. Walter Parallel Strategies for the Local Biological Sequence Alignment in a Cluster of Workstations.
Journal of Parallel and Distributed Computing 67(2):170185, Elsevier 2007.

2006
 D.M. MuñozArboleda, C. H. Llanos, M. AyalaRincón and R.H. van Els, Implementation, Simulation and Validation of Dispatching Algorithms for Elevator Systems. IEEE Proc. ReConFig'06, 2006.
Coauthor of ReConFig 2004, 2005 and 2006 papers granted with the
Synplicity award for best latinamerican R&D group on ReConFigurable Computing design
 D.L. Ventura, M. AyalaRincón and F. Kamareddine, Explicit Substitutions Calculi with Explicit Eta Rules which Preserve Subject Reduction, (postscript, PDF). In preproc. Brazilian Workshop on Logical and Semantic Frameworks, with Applications  LSFA'06, pp 115, 2006.
 D.M. MuñozArboleda, C. H. Llanos, M. AyalaRincón and R.P. Almeida, Implementation of Dispatching Algorithms for Elevator Systems using Reconfigurable Architectures. ACM Proc. 19th Symposium on Integrated Circuits and System Design  SBCCI 06, pp 3237, Ouro Preto, Brasil, (Aug 28  Sep 01, 2006).
 M. AyalaRincón and T. M. Sant'Ana, SAEPTUM: Verification of ELAN Hardware Specifications using the Proof Assistant PVS. ACM Proc. 19th Symposium on Integrated Circuits and System Design  SBCCI 06, pp 125130, Ouro Preto, Brasil, (Aug 28  Sep 01, 2006).
 F.L.C. de Moura, M. AyalaRincón and F. Kamareddine, SUBSEXPL: a Tool for Simulating and Comparing Explicit Substitutions Calculi, Journal of Applied and Nonclassical Logics 16(12):119150, Special Issue on Implementation of Logics (selected papers of IWIL4 and IWIL5), edited by Boris Konev, Renate Schmidt and Stephan Schulz, (PDF), 2006.
 M. AyalaRincón, C. Llanos, R. P. Jacobi, and R. Hartenstein, Prototyping Time and Space Efficient Computations of Algebraic Operations over Dynamically Reconfigurable Systems Modeled by RewritingLogic, in ACM Transactions on Design Automation of Electronic Systems TODAES 11(2):251281 (communicated by Ting Ting Hwang) 2006.

2005
 E.F.O. Sandes, A.C.M.A. de Melo, M. AyalaRincón, Comparação Paralela Exata de Sequências Biolólogicas Longas en Clusters de Computadores. I2TS 2005.
 R. P. Jacobi, M. AyalaRincón, L. G. A. Carvalho, C. Llanos and R. Hartenstein, Reconfigurable Systems for Sequence Alignment and for General Dynamic Programming. Genetics and Molecular Research, 4(3):543552, 2005.
 André Braga, C. Llanos, M. AyalaRincón and R. P. Jacobi, VANNGen: a Flexible CAD Tool for Hardware Implementation of Artificial Neural Networks, (Postscript, 370 KB). In IEEE Computer Society, Int. Conf. on Reconfigurable Computing and FPGAs  ReConFig05, 2005.
 T. M. Sant'Ana and M. AyalaRincón, Verification of Rewrite Based Specifications using Proof Assistants,
(pdf, postscript), in Proc. XXXI CLEI, pp 699710, 2005.
 C. Morra, J. Becker, M. AyalaRincón and R. Hartenstein, FELIX: Using RewritingLogic for Generating Functionally Equivalent Implementations, in Proc. IEEE CS 15^{th} International Conference on FieldProgrammable Logic and Applications FPL 2005, pp. 2530.
 R. de C. Miranda and M. AyalaRincón, A Modification of the LandauVishkin Algorithm Computing Longest Common Extensions via Suffix Arrays, (pdf).
 A. Boukerche, A.C.M.A. de Melo, M. AyalaRincón, T. M. Sant'ana, Parallel Strategies for Local Biological Sequence Alignment in a Cluster of Workstations. IPDPS 2005, IEEE Computer Society, 4th International Workshop on Performance Modeling, Evaluation, and Optimization of Parallel and Distributed Systems (PMEOPDS 2005), 2005.
 A. Boukerche, A.C.M.A. de Melo, M. AyalaRincón, T. M. Sant'ana, Parallel SmithWaterman Algorithm for Local DNA Comparison in a Cluster of Workstations. Proc. 4^{th} Experimental and Efficient Algorithms  WEA 2005, SpringerVerlag, LNCS 3503, pp 464475, 2005.

F.L.C. de Moura, M. AyalaRincón and F. Kamareddine, SUBSEXPL: a Tool for Simulating and Comparing Explicit Substitutions Calculi. 5^{th} International Workshop on the Implementation of Logics held in conjunction with the Proc. 11^{th} Int. Conf. on Logic Programming Artificial Intelligence and Reasoning LPAR 2004, (Tutorial postscript version, PDF)
March 2005.
 F.L.C. de Moura, F. Kamareddine and M. AyalaRincón, SecondOrder Matching via Explicit Substitutions, (postscript, PDF). Proc. 11^{th} Int. Conf. on Logic Programming Artificial Intelligence and Reasoning LPAR 2004, F. Baader and A. Voronkov, Eds., SpringerVerlag, LNCS 3452, pp 433448, March 2005.
 M. AyalaRincón, F.L.C. de Moura and F. Kamareddine, Comparing and Implementing Calculi of Explicit Substitutions with EtaReduction, (Postscript, 277 KB). Annals of Pure and Applied Logic  WoLLIC 2002 selected papers, Ruy de Queiroz, Bruno Poizat and Sergei Artemov, Eds., Vol 134(1):541, 2005.

2004
 R. P. Jacobi, M. AyalaRincón, L. G. A. Carvalho, C. Llanos and R. Hartenstein, Reconfigurable Systems for Sequence Alignment and for General Dynamic Programming, (pdf. Proc. 3rd Brazilian Workshop on Bioinformatics  WOB 2004, pp 2532 Brasília D. F., Brasil, (Oct. 2022, 2004). Versão journal a aparecer em Genetics and Molecular Research, 2005.
 C. LLanos, R. P. Jacobi, M. AyalaRincón and R. Hartenstein, A Dynamically Reconfigurable System for SpaceEfficient Computation of the FFT, (postscritp, X MB; Pdf, X MB). Soc. Mex. Comp. Proc. International Conference on Reconfigurable Computing and FPGAs 2004  ReConFig'04, pp 360369, Colima, Mexico, (Sep 2021, 2004).
 M. AyalaRincón, R. P. Jacobi, L. G. A. Carvalho, C. Llanos and R. Hartenstein, Modeling and Prototyping Dynamically Reconfigurable Systems for Efficient Computation of Dynamic Programming Methods, (postscritp, X MB; Pdf, X MB). ACM Proc. 17th Symposium on Integrated Circuits and System Design  SBCCI 04, pp 248253 Porto Galhinas, Brasil, (Sep 711, 2004).
 F. Kamareddine, F. Monin and M. AyalaRincón, On automating the extraction of programs from termination proofs, (PDF, 250 KB). Colombian Journal of Computation, Vol 4(2):2948, 2004.

2003
 M. AyalaRincón and P. D. Conejo, A Linear Time Lower Bound on McCreight and General Updating Algorithms for Suffix Trees, in Algorithmica, 37(3):233241, SpringerVerlag, (communicated by F. P. Preparata), 2003.
 M. AyalaRincón, R. B. Nogueira, C. Llanos, R. P. Jacobi and R. Hartenstein, Efficient Computation of Algebraic Operations over Dynamically Reconfigurable Systems Specified by RewritingLogic Environments, (PDF). In IEEE CS press Proc. 23^{rd} SCCC, pp 6069, 2003..
 M. AyalaRincón and F. Kamareddine, On Applying the lambda s_{e}Style of Unification for SimplyTyped Higher Order Unification in the Pure lambda Calculus. Special Issue of WoLLIC 2001 selected papers, John T. Baldwin, Ruy J. G. B. de Queiroz and Edward H. Haeusler, Eds. Matemática Contemporânea, Vol. 24:122, 2003.
 M. AyalaRincón, R. B. Nogueira, R. P. Jacobi, C. Llanos and R. Hartenstein, Modeling a Reconfigurable System for Computing the FFT in Place via RewritingLogic, (postscritp, X MB; Pdf, X MB). In IEEE CS Press Proc. 16th Symposium on Integrated Circuits and System Design  SBCCI 03, pp 205210, São Paulo, Brasil, (Sep 811, 2003).
.
 R. Hartenstein, R. P. Jacobi, M. AyalaRincón and C. Llanos, Using RewritingLogic Notation for Functional Verification in DataStream Based Reconfigurable Computing, (postscritp, X MB; Pdf, X MB). In Forum on Specification and Design Languages  FDL 03, Frankfurt, Germany, (Sep 2326, 2003).
 M. AyalaRincón, R. Hartenstein, R. Maya Neto, R. P. Jacobi and C. Llanos, Architectural Specification, Exploration and Simulation Through RewritingLogic, (Postscript, 134 KB). Colombian Journal of Computation, Vol 3(2):2034, 2003.

2002
 M. AyalaRincón, A.F. da Fonseca, H.W. Poubel and J. de Siqueira, A Framework to Visualize Equivalences Between Computational Models of Regular Languages, Information Processing Letters, 84(1):516, Elsevier 2002.
 F. Kamareddine, F. Monin and M. AyalaRincón, On automating the extraction of programs from proofs using product types , (Postscript, 380 KB). In PreProc. 9^{th} Workshop on Logic, Language, Information and Computation  WoLLIC 2002, pages 215234, Rio de Janeiro, Brasil, July 30  August 2, 2002. In Vol. 67 of the Elsevier ENTCS.
 M. AyalaRincón, F.L.C. de Moura and F. Kamareddine, Comparing Calculi of Explicit Substitutions with EtaReduction, (Postscript, 350 KB). In PreProc. 9^{th} Workshop on Logic, Language, Information and Computation  WoLLIC 2002, pages 7696, Rio de Janeiro, Brasil, July 30  August 2, 2002. In Vol. 67 of the Elsevier ENTCS.
 M. AyalaRincón, R. Maya Neto, R. P. Jacobi, C. Llanos and R. Hartenstein, Applying ELAN Strategies in Simulating Processors over Simple Architectures, (Postscript, 290 KB) (PDF, 312 KB). In Proc. 2nd Int. Workshop on Reduction Strategies in Rewriting and Programming  WRS'02, pages 127141, Copenhagen, Denmark, July 21, 2002. Power point Talk. In Vol. 70, issue 6 of the Elsevier ENTCS
 M. AyalaRincón and I. E. T. de Araújo, Unification Modulo Presburger Arithmetic and Other Decidable Theories, Colombian Journal of Computation, 2(2):719, 2001. (Gziped Postscript, 87 KB).

2001
 L. M. R. Gadelha and M. AyalaRincón, An Efficient Strategy for WordCycle Completion of Finitely Presented Groups In Proc. XXI International Conference of the Chilean Computer Science Society  SCCC 2001, pages 8085, Punta Arenas, Chile, November 2001. IEEE CS press, 2001 (Postscript, 95 KB).
 M. AyalaRincón and F. Kamareddine, On Applying the lambda s_{e}Style of Unification for SimplyTyped Higher Order Unification in the Pure lambda Calculus, In PreProceedings 8^{th} Workshop on Logic, Language, Information and Computation  WoLLIC 2001, pages 4154, Brasília, Brazil, July 31  August 3, 2001 (Postscript file of the talk).
 A.F. da Fonseca, A.H.R. da Silva, M. AyalaRincón, H.W. Poubel and J. de Siqueira, Animation of Relations between Computational Models and Their Language Representations, (Gziped Postscript, 64 KB). Bulletin of The European Association for Theoretical Computer Science  EATCS, 74:235241, June 2001.
 M. AyalaRincón, and F. Kamareddine, Unification via the Lambda s_{e}Style of Explicit Substitutions, The Logic Journal of the Interest Group on Pure and Applied Logics (IGPL), 9(4):489523, Oxford University Press, 2001.

2000
 M. AyalaRincón, and C. Muñoz, Explicit Substitutions and All That, postscript version. Colombian Journal of Computation, 1(1):4771, 2000. Also available as NASA ICASE Technical Report 200045.
 M. AyalaRincón, and F. Kamareddine, Strategies for SimplyTyped Higher Order Unification via lambda s_{e}Style of Explicit Substitution, in Proc. The Third International Workshop on Explicit Substitutions Theory and Applications to Programs and Proofs (WESTAPP 2000), pages 317. Held in conjunction with RTA2000, Norwich, England, 1013 July 2000.
 M. AyalaRincón, and F. Kamareddine, Unification via lambda s_{e}Style of Explicit Substitution, in Proc. 2nd International Conference on Principles and Practice of Declarative Programming (PPDP 2000), pages 163174, ACM Press. Held as part of PLI 2000, Montreal, Canada 1722 September 2000. (Talk (Postscript ), 355 KB)

1999
 M. AyalaRincón, ChurchRosser Property for Conditional Rewriting Systems with Builtin
Predicates as Premises, chapter in Frontiers of Combining Systems 2 (Studies in Logic and Computation, 7), Dov M. Gabbay and Maarten de Rijke, editors, Research Studies Press/Wiley, 1738, 1999.
Click here to order the book at
amazon.com.
 M. AyalaRincón and F. Kamareddine, Higher Order Unification via lambda s_{e}Style of Explicit Substitution, Technical Report ULTRA Group ( Useful Logics, Type Theory, Rewriting Systems and Their Applications), CEE, HeriotWatt University, Edinburgh, Scotland ( Link to ULTRA publications, You will find link to postscript file 600 KB). 53 pages, December 1999.

1998
 M. AyalaRincón and L. M. Gadelha:
Some Applications of (Semi)Decision Algorithms for Presburger Arithmetic in Automated Deduction based on
Rewriting Techniques ,
in La Revista de la Sociedad Chilena de Ciencia de la Computación , 2(1):1423 1997 (Edited in June 1998).
 M. AyalaRincón and P. D. Conejo, A Linear Time Lower Bound on
Updating Algorithms for Suffix Trees, in Proc. String Processing
and Information Retrieval: A South American Symposium, IEEE Computer Society, Santa Cruz de La
Sierra, Bolivia. September 1998.
 M. AyalaRincón, ChurchRosser Property for Conditional Rewriting Systems with Builtin
Predicates as Premises, in Proc. Frontiers of Combining Systems, Amsterdam, Holland. October 1998. See chapter version in 1999.
 I. E. T. de Araújo and M. AyalaRincón, An Algorithm for General Unification Modulo Presburger Arithmetic, in First Brazilian Workshop on Formal Methods, Porto Alegre, Brasil. October 1998.
 M. AyalaRincón:
A Deductive Calculus for Conditional Equational Systems with
Builtin Predicates as Premises,
in Revista Colombiana de Matemáticas 31(2):7798, 1997 (Edited in December 1998).
See paper in the nearest EMIS mirror: Brasil, Germany or
USA.

1997
 M. AyalaRincón:
A Deduction Procedure for Conditional Rewriting Systems with Builtin Predicates ,
in Proc. SEMISH'97, Brasília, Brasil, August 1997 (Gziped Postscript, 74 KB).
 L. M. Gadelha and M. AyalaRincón:
Métodos de Decisão para a Aritmética de Presburger na Dedução Automãtica com Técnicas de Reescrita ,
Abstract CNMAC'97 (XX Congresso Nacional de Matemática Aplicada e Computacional), Gramado, Brasil, September 1997 (Gziped Postscript, 24 KB). In Portuguese.
 L. M. Gadelha and M. AyalaRincón:
Applications of Decision Algorithms for Presburger Arithmetic in Rewrite Automated Deduction ,
in Proc. PANEL'97 (XXIII Latin American Conference on Informatics), Valparaíso, Chile, November 1997 (Gziped Postscript, 56 KB).

1996
 M. AyalaRincón:
Fundamentos da Programação Lógica e Funcional  O princípio de resolução e a teoria de reescrita ,
Course notes (in Portuguese), Dept. Mathematics, Univ. Brasilia. First version, Jan. 1996; Second version, Dec. 1997; Third version, Dec. 1998; Fourth version, Dec. 2000; Fifth version, March 2001; Sixth version, March 2002; Seventh version March 2003; Eight version, March 2004 (Postscript, 1.6 MB; PDF, 2.2 MB). In Portuguese.
 M. AyalaRincón:
Transforming CRSs into TRSs  About Elimination of the Conditions , in Proc. PANEL'96 (XXII Latin American Conference on Informatics), Bogotá, Colombia, June 1996
(Gziped Postscript, 77 KB).
 M. AyalaRincón:
Sistemas de Reescrita de Termos  O Modelo de Computação Funcional e suas Aplicações ,
Survey prepared for JAI'96 (XV Jornada de Atualização em Informática do XVI Congresso da Sociedade Brasileira de Computação), Recife, Brasil, August 1996 (Gziped Postscript, 166 KB). In Portuguese.
 L. M. Gadelha and M. AyalaRincón:
Aplicação de Métodos de Programação Linear Inteira para Decição na Teoria da Aritmética de Presburger ,
Abstract CNMAC'96 (XIX Congresso Nacional de Matemática Aplicada e Computacional), Goiânia, Brasil, September 1996 (Gziped Postscript, 24 KB). In Portuguese.

1995
 M. AyalaRincón:
A Note on Confluence of Term Rewriting Systems
under Joinability of Critical Pairs in One Step of Parallel Reduction
 Abstract,
Presented at 11th British Colloquium for Theoretical Computer Science, Swansea, Wales, April 1995
(Compressed Postscript, 23 KB).
 M. AyalaRincón:
A Deductive Calculus for Conditional Equational Systems with
Builtin Predicates as Premises,
Abstract in Proc. X Latin American Symposium on Mathematical Logic, Bogotá, Colombia, July 1995 (Compressed Postscript, 90 KB).
 M. AyalaRincón:
Embedding Builtin Predicates as Premises of
Rules of Conditional Rewriting Systems  Abstract,
Presented at 2nd Workshop on Logic, Language,
Information and Computation, Recife, Brasil, July 1995 (Compressed Postscript, 20 KB). Extended work (submitted) (Gziped Postscript, 100 KB).
 M. AyalaRincón:
Confluence of Term Rewriting Systems under Joinability of Critical Pairs in One Step of Parallel Reduction,
in Proc. SEMISHPANEL'95 (XXI Latin American Conference on Informatics), Canela, Brasil, JulyAugust 1995 (Compressed Postscript, 69 KB).
 M. AyalaRincón:
A Deductive Calculus for Conditional Equational Systems with
Builtin Predicates as Premises  Extended Abstract,
in Proc. XV International Conference of the Chilean Computer Science Society, Arica, Chile, October 1995 (Gziped Postscript, 74 KB).
 M. AyalaRincón:
Conditional Rewriting Systems with Builtin Predicates and Conjunctions of Standard Premises as Conditions,
Technical Report, Dept. Mathematics, Univ. Brasilia, Oct. 1995 (Gziped Postscript, 103 KB).

1994
 M. AyalaRincón:
Confluence of Conditional Rewriting Systems with Builtin Predicates and Standard Premises as Conditions,
in Proc. SEMISH'94, Caxambú, Brasil, JulyAugust 1994 (Compressed Postscript, 82 KB).

1993
 M. AyalaRincón:
Problemas actuales en el campo de la reescritura,
in Revista Escuela Colombiana de Ingeniería, 4(10):2731 JanuaryMarch 1993. In Spanish
 M. AyalaRincón:
Expressiveness of Conditional Equational Systems with Builtin Predicates,
PhD thesis under the supervision of Prof. Dr. K. Madlener, Fachbereich Informatik, Universität Kaiserslauten, Germany, December 1993. In English.
ayala NOSP@M mat.unb.br