Reports and Publications M. Ayala-Rincón

See also: MathSciNet DBLP IEEE ACM Scopus

Work in progress

• D. Nantes Sobrinho, M. Fernández and M. Ayala-Rincón A Proof of Polynomiality of the Elementary Deduction Problem for Electronic Purse Protocols with Blind Signatures, PDF. In preparation, 2011.
• Y.S. Rego and M. Ayala-Rincón Formalization in PVS of Balancing Properties Necessary for the Security of the Dolev-Yao Cascade Protocol Model, (pdf, Full PVS Theory: version PVS 5.n, version PVS 6.0). In preparation, 2012.
• R. de C. Miranda, M. Ayala-Rincón and Leon Solon, Modifications of the Landau-Vishkin 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. Ayala-Rincón Second- and Third-Order Matching via Explicit Substitutions, (postscript, PDF). In preparation, 2006.
• M. Ayala-Rincón and V.A. Fernandes and A.L. Galdino, Geometrical Specification using Dependent Types in PVS, (pdf, postscript). In preparation, 2005.
• M. Ayala-Rincón, R. Hartenstein, R. P. Jacobi and C. Llanos, Designing Arithmetic Digital Circuits via Rewriting-Logic, (Postscript, 370 KB). In preparation, 2004.
• M. Ayala-Rincón, H. W. Poubel and R. B. Nogueira Visualizing Relations Between Computational Models and Grammars of Context-Free Languages, (ps, 250 KB; PDF, 250 KB). In preparation, 2004.

2013

• D.M. Muñoz-Arboleda, C. H. Llanos, L. Coelho and M. Ayala-Rincón, Hardware-based Parallel Firefly Algorithm for Embedded Applications, NASA/ESA Conference on Adaptive Hardware and Systems. Accepted.
• J. Arias-García, A. Braga, C.H. Llanos, M. Ayala-Rincó, 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 2013). doi, 2013.

2012

• D.M. Muñoz-Arboleda, C. H. Llanos, L. Coelho and M. Ayala-Rincó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. Arias-Garcia, C. H. Llanos, M. Ayala-Rincó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. Arias-Garcia, C. H. Llanos, M. Ayala-Rincón and R. P. Jacobi , FPGA implementation of large-scale Matrix Inversion using single, double and custom floating-point precision. In: VIII Southern Conference on Programmable Logic SPL 2012, 2012, IEEE Proc. SPL 2012, 2012. p. 1-6. (doi)
• M. Ayala-Rincón Reusing Formal Proofs Through Isomorophisms. Invited Talk LACREST 2012 (PDFs abstract Proc. LACREST 2012 talk ).
• D. Saad and M. Ayala-Rincón A Compressed suffix array based index with succinct longest common prefix information. Short version accepted BSB 2012.
• A.C. Rocha Oliveira and M. Ayala-Rincón Formalizing the Confluence of Orthogonal Rewriting Systems. Presented in LSFA 2012. EPTCS Vol. 113:145-152, 2013 (doi, Extended Version, PVS tgz file)
• D. Nantes Sobrinho, M. Fernández and M. Ayala-Rincón Elementary Deduction Problem for Locally Stable Theories with Normal Forms, PDF. Presented in LSFA 2012. EPTCS Vol. 113:45-60, 2013 (doi)
• J.L. Soncco-Álvarez and M. Ayala-Rincó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:119-133, 2013 (doi) .
• T.A. de Lima and M. Ayala-Rincón Complexity of Reversal Distance and other General Metrics on Permutation Groups, PDF. 7CCC 2012. (doi)
• J.L. Soncco-Álvarez and M. Ayala-Rincó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. Ayala-Rincón, and A.L. Galdino A Formalization of the Theorem of Existence of First-Order Most General Unifiers, PDF. In Proc. Logical and Semantic Frameworks with Applications 2011.
• D.L. Ventura, M. Ayala-Rincó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. Ayala-Rincón , On the Formalization of the Property of Consequence of Orthogonal Term Rewriting SystemJ. Presented at EBL 2011
• Y.S. Rêgo and M. Ayala-Rincón ,Formalização em PVS de Propriedades de Balanceamento para o Modelo de Protocolos em Cascata de Dolev-Yao . Presented at EBL 2011
• D.M. Muñoz-Arboleda, C. H. Llanos, L. Coelho and M. Ayala-Rincón, Opposition-based Shuffled PSO with Passive Congregation Applied to FM Matching Synthesis . In Proc. IEEE Congress on Evolutionary Computation (CEC 2011) (doi)
• D.M. Muñoz-Arboleda, C. H. Llanos, L. Coelho and M. Ayala-Rincón, Hardware Particle Swarm Optimization with Passive Congregation for Embedded Applications. In Proc. 2011 VII Southern Conference on Programmable Logic (SPL) (doi)
• J. Arias-Garcia, R. P. Jacobi, C. H. Llanos and M. Ayala-Rincón, A Suitable FPGA Implementation of Floating-Point Matrix Inversion based on Gauss-Jordan Elimination. In Proc. 2011 VII Southern Conference on Programmable Logic (SPL) (doi)

2010

• A.L. Galdino and M. Ayala-Rincón A Formalization of the Knut-Bendix(-Huet) Critical Pair Theorem (doi, PVS files: TRS.tgz). J. of Automated Reasonning 45:301-325, 2010.
• D.M. Muñoz-Arboleda, D. F. Sanchez, C. H. Llanos and M. Ayala-Rincón, FPGA Based Floating-point Library for CORDIC Algorithms. In Proc. IEEE - SPL - VI Southern Programmable Logic Conference SPL 2010 doi, pp 55-60, 2010.
• D.N. Sobrino and M. Ayala-Rincó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. 218-231, 2010.
• A.B. Avelar, F.L.C. de Moura, M. Ayala-Rincón, and A.L. Galdino Verification of the Completeness of Unification Algoritms à la Robinson, PDF, doi. Proc. 17th WoLLIC, LNCS vol. 6188, pag. 110-124, 2010.
• D.L. Ventura, M. Ayala-Rincón and F. Kamareddine, Intersection type systems and explicit substitutions calculi , doi Proc. 17th WoLLIC, LNCS vol. 6188, pag. 232-246, 2010.
• R. B. Nogueira, A.C.A. Nascimento, F.L.C. de Moura and M. Ayala-Rincón, Formalization of Security Proofs Using PVS in the Dolev-Yao Model, (PDF, PVS files: verifD_Y.tgz)). Booklet Proc. Computability in Europe CiE, 2010.
• D.M. Muñoz-Arboleda, C. H. Llanos, L. Coelho and M. Ayala-Rincón, Accelerating the Shuffled Frog Leaping algorithm by parallel implementations in FPGAs. In Proc. IEEE Fifth International Conference on Bio-Inspired Computing: Theories and Applications (BIC-TA 2010) doi, pp 1526-34, 2010.
• D.M. Muñoz-Arboleda, C. H. Llanos, L. Coelho and M. Ayala-Rincón, Comparison between two FPGA implementations of the Particle Swarm Optimization algorithm for high-performance embedded applications. In Proc. IEEE Fifth International Conference on Bio-Inspired Computing: Theories and Applications (BIC-TA 2010) doi, pp 1637-45, 2010.
• D.M. Muñoz-Arboleda, D. F. Sanchez, C. H. Llanos and M. Ayala-Rincón, Tradeof of FPGA Design of a Floating-point Library for Arithmetic Operators. JICS Journal of Integrated Circuits and Systems 5:42-52, 2010.

2009

• D.M. Muñoz-Arboleda, C. H. Llanos, L. S. Coelho and M. Ayala-Rincón, Hardware Architecture for Particle Swarm Optimization using Floating-Point Arithmetic. In Proc. 9th Int. Conf. on Intelligent Systems Design and Applications ISDA´09
• D.L. Ventura, M. Ayala-Rincó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:69-82, 2010.
• D.L. Ventura, M. Ayala-Rincón and F. Kamareddine, Explicit Substitution Calculi with One Step Eta-reduction Decided Explicitly, (doi). In The Logical Journal of the IGPL, vol 17(6):697-718, 2009.
• D. F. Sanchez, D.M. Muñoz-Arboleda, C. H. Llanos and M. Ayala-Rincón, Parameterizable Floating-point Library for Arithmetic Operations in FPGAs. In Proc. 22nd Symposium on Integrated Circuits and System Design - SBCCI 09, 2009.
• D.M. Muñoz-Arboleda, D. F. Sanchez, C. H. Llanos and M. Ayala-Rincón, Tradeoffs of FPGA design of floating-point transcendental functions. In Proc. The 17th IFIP/IEEE International Conference on Very Large Scale Integration - VLSI-SOC 2009 .
• D.L. Ventura, M. Ayala-Rincó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. Ayala-Rincón A Formalization of Newman's and Yokouchi Lemmas in a Higher-Order Language Journal of Formalized Reasoning, 1(1):39-50, 2008.
• A.L. Galdino and M. Ayala-Rincó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ñoz-Arboleda, C. H. Llanos, M. Ayala-Rincó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):1309-1320, 2008. Doi
  
• D.M. Muñoz-Arboleda, C. H. Llanos, M. Ayala-Rincó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. Ayala-Rincó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. Ayala-Rincó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. Ayala-Rincón and F. Kamareddine, Principal Typing for Explicit Substitutions Calculi, (PDF, doi). Accepted for presentation and publication in the Proc. Logic and Theory of Algorithms, 4th Conference on Computability in Europe (CiE 2008), LNCS, Vol. 5028, pages 548-558, 2008.
• D.L. Ventura, M. Ayala-Rincó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. Ayala-Rincón and F. Kamareddine, Higher-Order Unification: a structural relation between Huet's method and the one based on explicit substitutions, Journal of Applied Logic 6(1):72-108, 2008.

2007

• A.L. Galdino and M. Ayala-Rincó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. Ayala-Rincón Formal Verification of an Optimal Air Traffic Conflict Detection and Recovery Algorithm, (pdf, PVS files: kb2d.tgz). In Proc. WoLLIC 2007, Springer-Verlag LNCS Vol. 4576, pages 177-188, 2007.
• D.L. Ventura, M. Ayala-Rincón and F. Kamareddine, Principal Typing for Explicit Substitutions Calculi, (PDF). Extended version of work in Proc. 4th Int. Workshop on Higher-Order Rewriting - HOR 2007, Ralph Mattes (Ed.), pages 45-59, 2007.
• A. Boukerche, A.C.M.A. de Melo, E. Sandes and M. Ayala-Rincón, An Exact Parallel Algorithm to Compare Very Long Biological Sequences in Clusters of Workstations. J. Cluster Computing 10:187-202, Springer 2007.
• M. Ayala-Rincón and B. T. de Abreu and J. de Siqueira, A Variant of the Ford-Johnson Algorithm that is more Space Efficient, Information Processing Letters 102(5):201-207, Elsevier 2007.
• A. Boukerche, A.C.M.A. de Melo, M. Ayala-Rincó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):170-185, Elsevier 2007.

2006

• D.M. Muñoz-Arboleda, C. H. Llanos, M. Ayala-Rincón and R.H. van Els, Implementation, Simulation and Validation of Dispatching Algorithms for Elevator Systems. IEEE Proc. ReConFig'06, 2006.
  Co-author of ReConFig 2004, 2005 and 2006 papers granted with the Synplicity award for best latin-american R&D group on ReConFigurable Computing design
• D.L. Ventura, M. Ayala-Rincón and F. Kamareddine, Explicit Substitutions Calculi with Explicit Eta Rules which Preserve Subject Reduction, (postscript, PDF). In pre-proc. Brazilian Workshop on Logical and Semantic Frameworks, with Applications - LSFA'06, pp 1-15, 2006.
• D.M. Muñoz-Arboleda, C. H. Llanos, M. Ayala-Rincó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 32-37, Ouro Preto, Brasil, (Aug 28 - Sep 01, 2006).
• M. Ayala-Rincó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 125-130, Ouro Preto, Brasil, (Aug 28 - Sep 01, 2006).
• F.L.C. de Moura, M. Ayala-Rincón and F. Kamareddine, SUBSEXPL: a Tool for Simulating and Comparing Explicit Substitutions Calculi, Journal of Applied and Non-classical Logics 16(1-2):119-150, Special Issue on Implementation of Logics (selected papers of IWIL-4 and IWIL-5), edited by Boris Konev, Renate Schmidt and Stephan Schulz, (PDF), 2006.
• M. Ayala-Rincón, C. Llanos, R. P. Jacobi, and R. Hartenstein, Prototyping Time and Space Efficient Computations of Algebraic Operations over Dynamically Reconfigurable Systems Modeled by Rewriting-Logic, in ACM Transactions on Design Automation of Electronic Systems TODAES 11(2):251-281 (communicated by Ting Ting Hwang) 2006.

2005

• E.F.O. Sandes, A.C.M.A. de Melo, M. Ayala-Rincón, Comparação Paralela Exata de Sequências Biolólogicas Longas en Clusters de Computadores. I2TS 2005.
• R. P. Jacobi, M. Ayala-Rincó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):543-552, 2005.
• André Braga, C. Llanos, M. Ayala-Rincó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. Ayala-Rincón, Verification of Rewrite Based Specifications using Proof Assistants, (pdf, postscript), in Proc. XXXI CLEI, pp 699-710, 2005.
• C. Morra, J. Becker, M. Ayala-Rincón and R. Hartenstein, FELIX: Using Rewriting-Logic for Generating Functionally Equivalent Implementations, in Proc. IEEE CS 15^th International Conference on Field-Programmable Logic and Applications FPL 2005, pp. 25-30.
• R. de C. Miranda and M. Ayala-Rincón, A Modification of the Landau-Vishkin Algorithm Computing Longest Common Extensions via Suffix Arrays, (pdf).
  • Complete version, in in Proc. XXXI CLEI, pp 41-50, 2005 (Talk).
  • Four page - extended abstract -, in Proc. Advances in Bioinformatics and Computational Biology BSB 2005, Springer-Verlag LNCS (LNBI) 3594:210-213, 2005.
• A. Boukerche, A.C.M.A. de Melo, M. Ayala-Rincó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 (PMEO-PDS 2005), 2005.
• A. Boukerche, A.C.M.A. de Melo, M. Ayala-Rincón, T. M. Sant'ana, Parallel Smith-Waterman Algorithm for Local DNA Comparison in a Cluster of Workstations. Proc. 4^th Experimental and Efficient Algorithms - WEA 2005, Springer-Verlag, LNCS 3503, pp 464-475, 2005.
• F.L.C. de Moura, M. Ayala-Rincó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. Ayala-Rincón, Second-Order 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., Springer-Verlag, LNCS 3452, pp 433-448, March 2005.
• M. Ayala-Rincón, F.L.C. de Moura and F. Kamareddine, Comparing and Implementing Calculi of Explicit Substitutions with Eta-Reduction, (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):5-41, 2005.

2004

• R. P. Jacobi, M. Ayala-Rincó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 25-32 Brasília D. F., Brasil, (Oct. 20-22, 2004). Versão journal a aparecer em Genetics and Molecular Research, 2005.
• C. LLanos, R. P. Jacobi, M. Ayala-Rincón and R. Hartenstein, A Dynamically Reconfigurable System for Space-Efficient 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 360-369, Colima, Mexico, (Sep 20-21, 2004).
• M. Ayala-Rincó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 248-253 Porto Galhinas, Brasil, (Sep 7-11, 2004).
• F. Kamareddine, F. Monin and M. Ayala-Rincón, On automating the extraction of programs from termination proofs, (PDF, 250 KB). Colombian Journal of Computation, Vol 4(2):29-48, 2004.

2003

• M. Ayala-Rincón and P. D. Conejo, A Linear Time Lower Bound on McCreight and General Updating Algorithms for Suffix Trees, in Algorithmica, 37(3):233-241, Springer-Verlag, (communicated by F. P. Preparata), 2003.
• M. Ayala-Rincón, R. B. Nogueira, C. Llanos, R. P. Jacobi and R. Hartenstein, Efficient Computation of Algebraic Operations over Dynamically Reconfigurable Systems Specified by Rewriting-Logic Environments, (PDF). In IEEE CS press Proc. 23^rd SCCC, pp 60-69, 2003..
• M. Ayala-Rincón and F. Kamareddine, On Applying the lambda s_e-Style of Unification for Simply-Typed 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:1-22, 2003.
• M. Ayala-Rincón, R. B. Nogueira, R. P. Jacobi, C. Llanos and R. Hartenstein, Modeling a Reconfigurable System for Computing the FFT in Place via Rewriting-Logic, (postscritp, X MB; Pdf, X MB). In IEEE CS Press Proc. 16th Symposium on Integrated Circuits and System Design - SBCCI 03, pp 205-210, São Paulo, Brasil, (Sep 8-11, 2003).
  • Talk presented by C. Llanos at 2^nd Dagstuhl Seminar on Dynamically Reconfigurable Systems: C. Llanos, M. Ayala-Rincón, R. B. Nogueira, R. P. Jacobi and R. Hartenstein, Modeling Dynamically Reconfigurable Systems via Rewriting-Logic, Dagstuhl, Germany, July 20-25, 2003
  .
• R. Hartenstein, R. P. Jacobi, M. Ayala-Rincón and C. Llanos, Using Rewriting-Logic Notation for Functional Verification in Data-Stream Based Reconfigurable Computing, (postscritp, X MB; Pdf, X MB). In Forum on Specification and Design Languages - FDL 03, Frankfurt, Germany, (Sep 23-26, 2003).
• M. Ayala-Rincón, R. Hartenstein, R. Maya Neto, R. P. Jacobi and C. Llanos, Architectural Specification, Exploration and Simulation Through Rewriting-Logic, (Postscript, 134 KB). Colombian Journal of Computation, Vol 3(2):20-34, 2003.

2002

• M. Ayala-Rincó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):5-16, Elsevier 2002.
• F. Kamareddine, F. Monin and M. Ayala-Rincón, On automating the extraction of programs from proofs using product types , (Postscript, 380 KB). In Pre-Proc. 9^th Workshop on Logic, Language, Information and Computation - WoLLIC 2002, pages 215-234, Rio de Janeiro, Brasil, July 30 - August 2, 2002. In Vol. 67 of the Elsevier ENTCS.
• M. Ayala-Rincón, F.L.C. de Moura and F. Kamareddine, Comparing Calculi of Explicit Substitutions with Eta-Reduction, (Postscript, 350 KB). In Pre-Proc. 9^th Workshop on Logic, Language, Information and Computation - WoLLIC 2002, pages 76-96, Rio de Janeiro, Brasil, July 30 - August 2, 2002. In Vol. 67 of the Elsevier ENTCS.
• M. Ayala-Rincó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 127-141, Copenhagen, Denmark, July 21, 2002. Power point Talk. In Vol. 70, issue 6 of the Elsevier ENTCS
• M. Ayala-Rincón and I. E. T. de Araújo, Unification Modulo Presburger Arithmetic and Other Decidable Theories, Colombian Journal of Computation, 2(2):7-19, 2001. (Gziped Postscript, 87 KB).

2001

• L. M. R. Gadelha and M. Ayala-Rincón, An Efficient Strategy for Word-Cycle Completion of Finitely Presented Groups In Proc. XXI International Conference of the Chilean Computer Science Society - SCCC 2001, pages 80-85, Punta Arenas, Chile, November 2001. IEEE CS press, 2001 (Postscript, 95 KB).
• M. Ayala-Rincón and F. Kamareddine, On Applying the lambda s_e-Style of Unification for Simply-Typed Higher Order Unification in the Pure lambda Calculus, In Pre-Proceedings 8^th Workshop on Logic, Language, Information and Computation - WoLLIC 2001, pages 41-54, Brasília, Brazil, July 31 - August 3, 2001 (Postscript file of the talk).
• A.F. da Fonseca, A.H.R. da Silva, M. Ayala-Rincó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:235-241, June 2001.
• M. Ayala-Rincó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):489-523, Oxford University Press, 2001.

2000

• M. Ayala-Rincón, and C. Muñoz, Explicit Substitutions and All That, postscript version. Colombian Journal of Computation, 1(1):47-71, 2000. Also available as NASA ICASE Technical Report 2000-45.
• M. Ayala-Rincón, and F. Kamareddine, Strategies for Simply-Typed 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 3-17. Held in conjunction with RTA2000, Norwich, England, 10-13 July 2000.
• M. Ayala-Rincó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 163-174, ACM Press. Held as part of PLI 2000, Montreal, Canada 17-22 September 2000. (Talk (Postscript ), 355 KB)

1999

• M. Ayala-Rincón, Church-Rosser Property for Conditional Rewriting Systems with Built-in 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, 17-38, 1999.
  Click here to order the book at amazon.com.
• M. Ayala-Rincó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, Heriot-Watt University, Edinburgh, Scotland ( Link to ULTRA publications, You will find link to postscript file 600 KB). 53 pages, December 1999.

1998

• M. Ayala-Rincó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):14-23 1997 (Edited in June 1998).
• M. Ayala-Rincó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. Ayala-Rincón, Church-Rosser Property for Conditional Rewriting Systems with Built-in 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. Ayala-Rincón, An Algorithm for General Unification Modulo Presburger Arithmetic, in First Brazilian Workshop on Formal Methods, Porto Alegre, Brasil. October 1998.
• M. Ayala-Rincón: A Deductive Calculus for Conditional Equational Systems with Built-in Predicates as Premises, in Revista Colombiana de Matemáticas 31(2):77-98, 1997 (Edited in December 1998).
  See paper in the nearest EMIS mirror: Brasil, Germany or USA.

1997

• M. Ayala-Rincón: A Deduction Procedure for Conditional Rewriting Systems with Built-in Predicates -, in Proc. SEMISH'97, Brasília, Brasil, August 1997 (Gziped Postscript, 74 KB).
• L. M. Gadelha and M. Ayala-Rincó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. Ayala-Rincó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. Ayala-Rincó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. Ayala-Rincó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. Ayala-Rincó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. Ayala-Rincó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. Ayala-Rincó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. Ayala-Rincón: A Deductive Calculus for Conditional Equational Systems with Built-in Predicates as Premises, Abstract in Proc. X Latin American Symposium on Mathematical Logic, Bogotá, Colombia, July 1995 (Compressed Postscript, 90 KB).
• M. Ayala-Rincón: Embedding Built-in 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. Ayala-Rincón: Confluence of Term Rewriting Systems under Joinability of Critical Pairs in One Step of Parallel Reduction, in Proc. SEMISH-PANEL'95 (XXI Latin American Conference on Informatics), Canela, Brasil, July-August 1995 (Compressed Postscript, 69 KB).
• M. Ayala-Rincón: A Deductive Calculus for Conditional Equational Systems with Built-in 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. Ayala-Rincón: Conditional Rewriting Systems with Built-in Predicates and Conjunctions of Standard Premises as Conditions, Technical Report, Dept. Mathematics, Univ. Brasilia, Oct. 1995 (Gziped Postscript, 103 KB).

1994

• M. Ayala-Rincón: Confluence of Conditional Rewriting Systems with Built-in Predicates and Standard Premises as Conditions, in Proc. SEMISH'94, Caxambú, Brasil, July-August 1994 (Compressed Postscript, 82 KB).

1993

• M. Ayala-Rincón: Problemas actuales en el campo de la reescritura, in Revista Escuela Colombiana de Ingeniería, 4(10):27-31 January-March 1993. In Spanish
• M. Ayala-Rincón: Expressiveness of Conditional Equational Systems with Built-in 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