Reports and Publications M. Ayala-Rincón

Work in progress

T.A. de Lima, A.L. Galdino, Bruno Berto de Oliveira Ribeiro, and M. Ayala-Rincón A Formalization of the General Theory of 1 Quaternions. (pdf) submitted 2024.
F.F. Serrano Suárez, T.A. de Lima, and M. Ayala-Rincón Combinatorial Applications of the Compactness Theorem. (pdf) submitted 2024.
M. Ayala-Rincón, M. Fernández, G. Ferreira Silva, Temur Kutsia and D. Nantes-Sobrinho, Certified First-Order AC-Unification and Applications. (pdf) submitted 2024.
M. Ayala-Rincón, D. M. Cerna, A. F. González Barragán, and T. Kutsia Equational Anti-Unification over Absorption Theories, ArXiv file, 2023.
T.A. de Lima and M. Ayala-Rincón NP-Completeness of Sorting Unsigned Permutations by Reversals . Note MAT/UnB pdf, Brasília, 2013.
M. Ayala-Rincón, B. Dundua, T. Kutsia and M. Marin Rewriting Logic from a rhoLog Point of View, Presented at LSFA 2017.
L. A. da Silveira, T. A. de Lima, and M. Ayala-Rincón On Reconfiguring Heterogeneous Parallel Island Models, See pdf and source at genoma site, Submitted 2023.
M. Ayala-Rincón and G.F. Silva, Why We Need Structured Proofs in Mathematics. Submitted extended abstract (pdf), Presentation in Workshop on Natural Formal Mathematics (affiliated to 13th Conference on Intelligent Computer Mathematics), NFM, 2020.

Editorial work: Proceedings and Special Issues

Naoki Kobayashi, Mauricio Ayala-Rincón: Selected Papers of the 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), Special Issue in Logical Methods in Computer Science vols. 18,19, 2023, (Preface) Contents
Mauricio Ayala-Rincón, and Samuel Mimram: Special Issue on Confluence. Mathematical Strucutures in Computer Science vol. 32(7), 2023, Contents
Mauricio Ayala-Rincón, and Eduardo Bonelli: Proc. 16th Logical and Semantic Frameworks with Applications LSFA 2021, EPTCS vol 357, 2022. Contents.
Mauricio Ayala-Rincón, and Philippe Balbiani: Special Issue on Unification. Mathematical Strucutures in Computer Science vol. 30(6), 2020, Contents
Mauricio Ayala-Rincón, and Samuel Mimram: Proceedings of the Ninth International Workshop on Confluence IWC 2020 (with system descriptions from CoCo 2020), pdf, 2020.
Mauricio Ayala-Rincón, Silvia Ghilezan, and Jakob Grue Simonsen: Joint Proceedings of HOR 2019 and IWC 2019 (with system descriptions from CoCo 2019), pdf, 2019.
Mauricio Ayala-Rincón, and César A. Muñoz: Special Issue of selected extended papers of the Eighth International Conference on Interactive Theorem Proving. Journal of Automated Reasoning vol. 63(2), 2019, Contents
Mauricio Ayala-Rincón, César A. Muñoz: Proc. 8th International Conference on Interactive Theorem Proving (ITP 2017). Springer LNCS vol. 10499, 2017
Mauricio Ayala-Rincón, Ian Mackie and Ugo Montanari: Special Issue of Logical and Semantic Frameworks with Applications (LSFA 2014). Theor. Comput. Sci. vol. 685, 2017. Contents
Mauricio Ayala-Rincó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 Ayala-Rincón, Eduardo Bonelli, Ian Mackie: Proc. 9th International Workshop on Developments in Computational Models (DCM 2013). EPTCS vol. 144, 2014. Contents
Mauricio Ayala-Rincó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 Ayala-Rincó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 Ayala-Rincón, Edward Hermann Haeusler: Special Issue of Logical and Semantic Frameworks, with Applications (LSFA 2007). Logic Journal of the IGPL vol. 17(5): 487-488, 2009. Contents
Mauricio Ayala-Rincó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

Books

M. Ayala-Rincón & Flávio L.C. de Moura, Applied Logic for Computer Scientists: Computational Deduction and Formal Proofs, Springer, 2017.

M. Ayala-Rincón & Flávio L.C. de Moura, Fundamentos da Programação Lógica e Funcional - O Princípio de Resolução e a Teoria de Reescrita -, Course Notes, Ed. UnB, December 2014. In Portuguese.

Tutorials and Talks

M. Ayala-Rincón Exemplifying Formal Mathematics Talk XVI Summer Workshop in Mathematics.
M. Ayala-Rincón Formalising Nominal Equational Reasoning Invited talk at The 37th International Workshop on Unification, UNIF 2023.
M. Ayala-Rincón Formalization of Algebraic Theorems in PVS Invited Talk at The 24th International Conference on Logic for Programming, Artificial Intelligence, and Automated Reasoning, LPAR 2023.
T. A. de Lima amd M. Ayala-Rincón Mechanizing Mathematics Ten hour course on the application of interactive proof assistants using PVS. Faculty of Exact and Natural Sciences, Universidad Nacional de Colombia - campus Manizales, May-Jun, 2023
Diagnóstico e recomendações automáticas: IA em decisões sociais - o problema de alinhamento - Slides, Palestra Semana Universitária 2022 da Universidade de Brasília.
Jeanna Matthews, Cansu Canca, Claude Kirchner - Round Table on Ethics in AI (moderated by M. Ayala-Rincón) Slides with Pre-cooked questions YouTube, IE/CIC/UnB, May 27th, 2022.
M. Ayala-Rincón and T. A. de Lima Formalizing Theorems with PVS Slides and code PVS Tutorial for Mathematicians Affiliated to XIV Summer Workshop in Mathematics, IE/UnB, 2022.
M. Ayala-Rincón and T. A. de Lima Formalização de Teoremas com Assistentes de Prova Slides and code PVS Tutorial for Mathematicians Affiliated to XXIX Semana do IME/UFG, 2021.
M. Ayala-Rincón, Matemática, "Inteligência" e Consciência da Computação. Youtube, Slides, Palestra Semana Universitária 2021 da Universidade de Brasília.
Formalization of Termination of Functional Specifications in PVS, Youtube Invited Talk, Annual meeting IFIP WG 1.6:Rewriting, part of FSCD 2021.
M. Ayala-Rincón, Invited Talk Nominal Equational Reasoning given in the 15^th Logical and Semantic Frameworks, with Applications - LSFA 2020, UFBA, Bahia, 27-28 August, 2020. Slides
M. Ayala-Rincón, D. Nantes-Sobrinho, and F.L.C. de Moura, Matemática da Computação. Youtube, Slides, Palestra motivação na Semana Universitária 2020 da Universidade de Brasília. motivação na Semana Universitária 2021 da Universidade de Brasília.
M. Ayala-Rincón and T. A. de Lima, Teaching Interactive Proofs to Mathematicians. PVS 7.0 source, model of tutorial. In Proceedings 9th International Workshop on Theorem Prover Components for Educational Software (ThEdu), 2020.
T. A. de Lima and M. Ayala-Rincón Interactively Proving Mathematical Theorems. PVS Tutorial for Mathematicians Affiliated to XII Sumer Workshop in Mathematics, UnB, 2020.
César Muñoz, Mariano Moscato and M. Ayala-Rincón PVS Class 2017 Affiliated to ITP 2017.
César Muñoz and M. Ayala-Rincón, Tutorial on Formalization of Rewriting and Termination with a Proof Assistant given in the 10^th International School on Rewriting - ISR 2018, Cali, Colombia, 30 July - 3 August 2018.
- Compressed file with foils of the four slots and exercises
M. Ayala-Rincón, Tutorial on Formal Reasoning with PVS given in the Nat@logic Reasoning School 2015, Natal, Brazil, 31 August - 1 September 2015.
- Tutorial foils
- PVS exercises
M. Ayala-Rincó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. Slides
M. Ayala-Rincó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.
- Tutorial foils
- PVS exercises

Publications by year

2023

C. Muñoz, M. Ayala-Rincón, M. Moscato, A. Dutle, A. Narkawicz, A.A. Almeida, A.B.A. da Silva and T.M. Ferreira Ramos Formal Verification of Termination Criteria for First-Order Recursive Functions - Extended Version, [Supercedes ITP 2021 paper (doi)] Journal of Automated Reasoning 67:40, 2023 (doi).
L. A. da Silveira, T. A. de Lima, J. B. de Barros, J. L. Soncco-Álvarez, C. H. Llanos, and M. Ayala-Rincón On The Behaviour of Parallel Island Models Genetic Algorithms, See source and data at genoma site, J. Applied Soft Computing, Volume 148, paper 110880, 2023 (doi).
N.B.F.Ferreira, M.M. Moscato, L. Titolo and M. Ayala-Rincón, A provably correct floating-point implementation of Well Clear Avionics Concepts The 23rd Int. Conf. on Formal Methods in Computer-Aided Design FMCAD 2023, pp. 237–246, TU Wien Academic Press, 2023 (doi).
M. Ayala-Rincón, M. Fernández, G. Ferreira Silva, Temur Kutsia and D. Nantes-Sobrinho, Nominal AC-matching. "Best Paper Award" . (Extended version pdf), In The 16th Conference on Intelligent Computer Mathematics, CICM 2023. Springer LNAI 14101, pp 53-68, 2023 (doi)
T.A. de Lima, A.B. Avelar, A.L. Galdino, and M. Ayala-Rincón Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms. (pdf, Pre-Proc., pp. 6-21) 18th Logical and Semantic Frameworks with Applications (LSFA), pp. 6-21, 2023.
M. Ayala-Rincón Formalisation of Nominal Equational Reasoning (IT) Extended abstract in Inf. Proc. 37th Int. Workshop on Unification, UNIF 2023 (INRIA HAL portal, Id. 04137801), 2023.
A.F. González Barragán, D.M. Cerna, . Ayala-Rincón, T. Kutsia On Anti-unification in Absorption Theories Extended abstract in Inf. Proc. 37th Int. Workshop on Unification, UNIF 2023 (INRIA HAL portal, Id. hal-04128203), 2023.
M. Ayala-Rincón, T. A. de Lima, A. Borges Avelar, and A. L. Galdino, Formalization of Algebraic Theorems in PVS (IT). In Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoningm LPAR, EPiC Series in Computing, vol. 94:1-10 (doi), 2023.
F.F. Serrano Suárez, T.A. de Lima, and M. Ayala-Rincón Mechanising Hall’s Theorem for Countable Graphs. Presented at 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoningm LPAR, EasyChair Preprint No 10365:1-14 pdf, 2023.

2022

da Silveira, L. A. & de Lima, T. A. & Ayala-Rincón, M. Reconfigurable Heterogeneous Parallel Island Models, See pdf and source at genoma site, In IEEE Symposium Series on Computational Intelligence (SSCI), 2022 (doi)
T.M. Ferreira Ramos, A.A. Almeida, and M. Ayala-Rincón Formalization of the Computational Theory of a Turing Complete Functional Language Model. Journal of Automated Reasoning, Vol. 66, pages 1031–1063, (doi) 2022.
J. B. de Barros, N. Anantharajaiah, M. Ayala-Rincón, C.H. Llanos, and J. Becker The Impact of Formulation of Cost Function in Task Mapping Problem on NoCs using bio-inspired based-Metaheuristics. Journal version of paper presented at IEEE Nordic Circuits and Systems Conference - NorCAS 2020. Microprocessors and Microsystems Volume 94, 104668, Oct 2022 (doi).
F.F. Serrano Suárez, T.A. de Lima, and M. Ayala-Rincón Hall’s Theorem for Enumerable Finite Sets . pdf, Proc. 15th Intelligent Computer Mathematics CICM, Springer Nature LNAI 13467:107–121, 2022 (doi).
Daniel S. N. Nunes, Felipe A. Louza, Simon Gog, Mauricio Ayala-Rincón, Gonzalo Navarro Grammar Compression By Induced Suffix Sorting. ArXiv version, ACM Journal of Experimental Algorithmics, Vol. 27, Article No.: 1.1 pp 1–33, Dec 2022 (doi).
M. Ayala-Rincón, M. Fernández, G.F. Silva, and D. Nantes-Sobrinho, A Certified Algorithm for AC-Unification. Formal Structures for Computation and Deduction FSCD, 8:1-8:21, 2022 (doi).

2021

M. Ayala-Rincón, W. de Carvalho-Segundo, M. Fernández, G.F. Silva, and D. Nantes-Sobrinho, Formalising Nominal C-Matching through Unification with Protected Variables. Math. Struct. in Comp. Sci., Vol 31(3):286-311, 2021 (doi).
da Silveira, L. A. & de Lima, T. A. & Soncco-Álvarez, J. L. & Ayala-Rincón, M. Heterogeneous Parallel Island Models (pdf author version, Source and Data). , See pdf and source at genoma site. 2021 IEEE Symposium Series on Computational Intelligence (SSCI). (doi).
T. A. de Lima, A. L. Galdino, A. Borges Avelar, and M. Ayala-Rincón, Formalization of Ring Theory in PVS - Isomorphism Theorems, Principal, Prime and Maximal Ideals,Chinese Remainder Theorem. Source: PVS 7.1 files, (pdf). Journal of Automated Reasoning Vol. 65:1231–1263, (doi), 2021.
M. Ayala-Rincón, M. Fernández, D. Nantes-Sobrinho and D. Vale Nominal Equational Problems, In Proc. 24th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2021) , Springer, LNCS vol. 12650:22-41 (doi), 2021.
E. Álvarez-Mamani, L. Enciso-Rodas, M. Ayala-Rincón and José Luis Soncco-Álvarez, Parallel Social Spider Optimization Algorithms with Island Model for the Clustering Problem. Presented at 7th International Conference on Information Management and Big Data, 3rd Place Google Award: SIMBig vs Covid, (doi), 2020.
C. Muñoz, M. Ayala-Rincón, M. Moscato, A. Dutle, A. Narkawicz, A.A. Almeida, A.B.A. da Silva and T.M. Ferreira Ramos Formal Verification of Termination Criteria for First-Order Recursive Functions, in Proc. ITP 2021 (12th Int. Conference on Interactive Theorem Proving) (LIPIcs pdf at NASA LarC FM), (doi) 2021.

2020

M. Ayala-Rincón and T. A. de Lima, Teaching Interactive Proofs to Mathematicians. In Proceedings 9th International Workshop on Theorem Prover Components for Educational Software (ThEdu), 2020, (doi) .
J. B. de Barros, N. Anantharajaiah, M. Ayala-Rincón, C.H. Llanos, and J. Becker A Study of the Impact of Formulation of CostFunction in Task Mapping Problem on NoCs. Proc. IEEE Nordic Circuits and Systems Conference - NorCAS 2020, (doi).
L. A. da Silveira, J. L. Soncco-Álvarez, T. A. de Lima, and M. Ayala-Rincón Behaviour of Bioinspired Algorithms in Parallel Island Models See extended version at genoma site. 2020 IEEE Congress on Evolutionary Computation CeC 2020, (doi).
A.A. Almeida, and M. Ayala-Rincón Formalizing the Dependency Pairs Criterion for Innermost Termination. Associated formalization available as part of the PVS term rewriting systems theory at trs). Version presented at SBMF 2019 ArXiv. Journal version in Science of Computer Programming (doi), 2020.
M. Ayala-Rincón, M. Fernández and D. Nantes-Sobrinho On Nominal Syntax and Permutation Fixed Points. Logical Methods in Computer Science 16(1):19:1-36, 2020 (arXiv / pdf LMCS / doi)
M. Ayala-Rincón, M. Fernández, D. Nantes-Sobrinho and D. Vale On Solving Nominal Disunification Constraints, Revised papers Proc. LSFA 2019, ENTCS Vol. 348:Pages 3-22, 2020 (doi).
M. Ayala-Rincón, M. Fernández, D. Nantes-Sobrinho and D. Vale. An Investigation into General Nominal Equational Problems, Proc. 34th International Workshop on Unification (UNIF), Temur Kutsia and Andrew M. Marshall (Eds.), RISC-Linz Report Series No. 20-10, pp.3:1-8, 2020.
J. Barreto, C.H. Llanos, and M. Ayala-Rincón Application of an Adaptive Genetic Algorithm for Task Mapping Optimisation on a Wromhole-based Real-time Network-on-chip , 2019 IX Brazilian Symposium on Computing System Engineering (SBESC), IEEE Xplore 2020 (doi).
M. Ayala-Rincón, M. Fernández, G. Ferreira Silva and D. Nantes-Sobrinho A Certified Functional Nominal C-Unification Algorithm. In Post-proceddings Logic-Based Program Synthesis and Transformation (LoPSTR 2019), Springer, LNCS vol. 12042:1-16, (PVS formalisation in site Nominal ), (doi), 2020.

2019

M. Ayala-Rincón, M. Fernández, G. Ferreira Silva and D. Nantes-Sobrinho A Certified Functional Nominal C-Unification Algorithm. Presented at LOPSTR 2019 (LOPSTR Informal pre-proceedings ). Extended version: (pdf).
A.A. Almeida, A.C. Rocha-Oliveira, T.M.F. Ramos, F.L.C. de Moura, and M. Ayala-Rincón The Computational Relevance of Formal Logic Through Formal Proofs. In FMTea 2019, Proc. FMTea, Springer LNCS vol. 11758:81-96, 2019 (doi).
L.A. da Silveira, J.L. Soncco-Álvarez, T.A. de Lima and M. Ayala-Rincón Parallel Island models Genetic Algorithms applied in NP-Hard problems (pdf at genoma project page). 2019 IEEE Congress on Evolutionary Computation CeC 2019, (doi).
M. Ayala-Rincón, M. Fernández and G. Ferreira Silva Formalising Nominal AC-Unification. Presented at UNIF 2019.
M. Ayala-Rincón, E. Bonelli, J. Edi and A. Viso Typed Path Polymorphism, Theoretical Computer Science Vol. 781:111-130 (doi), 2019.
M. Ayala-Rincón, W. de Carvalho-Segundo, M. Fernández and D. Nantes-Sobrinho, and A.C. Rocha-Oliveira A Formalisation of Nominal alpha-equivalence with A, C, and AC Function Symbols. (Coq formalisation , PDF), Theoretical Computer Science Vol. 781:3-23 (doi), 2019.
J.L. Soncco-Álvarez, D.M. Muñoz and M. Ayala-Rincón Opposition-Based Memetic Algorithm and Hybrid Approach for Sorting Permutations by Reversals, Evolutionary Computation Vol. 27(2):229-265 (doi), 2019.

2018

M. Ayala-Rincón, W. de Carvalho-Segundo, M. Fernández, and D. Nantes-Sobrinho, A Formalisation of Nominal C-Matching through Unification with Protected Variables. Presented at 13th Logical and Semantic Frameworks with Applications (LSFA) (Pre-proceedings), pages 28-41, 2018. ENTCS 344:47-65, 2019 (doi).
B. de Assis Delboni, M. Ayala-Rincón, and D. Nantes-Sobrinho, Topological Graphs and Combinators. Presented at 13th Logical and Semantic Frameworks with Applications (LSFA) (extended version), pages 115-127, 2018.
L.A. da Silveira, J.L. Soncco-Álvarez, T.A. de Lima and M. Ayala-Rincón Parallel Multi-Island Genetic Algorithms for Sorting Unsigned Genomes by Reversals. In Proc. 2018 Congress on Evolutionary Computation (CEC), (available at EA genoma web page), (doi, IEEExplore link), 2018.
César Muñoz and M. Ayala-Rincón, Tutorial on Formalization of Rewriting and Termination with a Proof Assistant given in the 10^th International School on Rewriting - ISR 2018, Cali, Colombia, 30 July - 3 August 2018.
- Compressed file with foils of the four slots and exercises
M. Ayala-Rincón, M. Fernández and D. Nantes-Sobrinho Fixed-Point Constraints for Nominal Equational Unification. In Proc. 3rd International Conference on Formal Structures for Computation and Deduction (FSCD), LIPIcs, vol. 108 (doi), 2018.
T.M. Ferreira Ramos, C. Muñoz, M. Ayala-Rincón, M. Moscato, A. Dutle, and A. Narkawicz Formalization of the Undecidability of the Halting Problem for a Functional Language, In Proc. WoLLIC 2018, Springer, LNCS vol. 10944:196-209, (doi), 2018.
M. Ayala-Rincón, W. de Carvalho-Segundo, M. Fernández and D. Nantes-Sobrinho Nominal C-Unification. In Post-proceddings Logic-Based Program Synthesis and Transformation (LOPSTR 2017), Springer, LNCS vol. 10855:235-251, (Coq formalisation / OCaml implementation , PDF extended version), (doi), 2018.
M. Ayala-Rincón, M. Fernández, A. C. Rocha-Oliveira and D.L. Ventura Nominal essential intersection types. Theoretical Computer Science 737:62-80 (doi), 2018.
Daniel Saad Nogueira Nunes, Felipe A. Louza, Simon Gog, M. Ayala-Rincón and Gonzalo Navarro A Grammar Compression Algorithm based on Induced Suffix Sorting, In IEEE Proc. Data Compression Conference - DCC, pages 42-51 (ArXiv version), (doi), 2018.
T.A. de Lima and M. Ayala-Rincón On the average number of reversals needed to sort signed permutations, Discrete Applied Mathematic 235:59-80 (doi), 2018.

2017

M. Ayala-Rincón, W. de Carvalho-Segundo, M. Fernández and D. Nantes-Sobrinho Nominal C-Unification, Pre-Proceedings ArXiv version presented at LOPSTR, 2017.
M. Ayala-Rincón, W. de Carvalho-Segundo, M. Fernández and D. Nantes-Sobrinho On solving nominal fixpoint equations - pdf, In Proc. 11th International Symposium on Frontiers of Combining Systems - FroCoS, Springer Nature LNAI vol. 10483:209-226, (doi), 2017.
L.A. da Silveira, J.L. Soncco-Álvarez and M. Ayala-Rincón Parallel Genetic Algorithms with Sharing of Individuals for Sorting Unsigned Genomes by Reversals. 2017 IEEE Congress on Evolutionary Computation (CEC), 741-748 (doi), 2017.
J.L. Soncco-Álvarez and M. Ayala-Rincón Variable Neighborhood Search for the Large Phylogeny Problem using Gene Order Data. Presented at 2017 IEEE Congress on Evolutionary Computation (CEC), pp 59-66 (doi), 2017.
M. Ayala-Rincón, W. de Carvalho-Segundo, M. Fernández and D. Nantes-Sobrinho A Formalisation of Nominal alpha-equivalence with A and AC Function Symbols ENTCS 332:21-38 (doi), 2017.
M. Ayala-Rincón, M. Fernández and D. Nantes-Sobrinho Intruder Deduction Problem for Locally Stable Theories with Normal Forms and Inverses. Theoretical Computer Science 672:64-100 (doi), 2017.
A.C. Rocha-Oliveira, A.L. Galdino and M. Ayala-Rincón Confluence of Orthogonal Term Rewriting Systems in the Prototype Verification System. Journal of Automated Reasoning 58(2):231-251 (doi), 2017.

2016

M. M. Ayala-Rincón Formalising Confluence in PVS. Proc. of the Eleventh International Workshop on Developments in Computational Models, DCM 2015. EPTCS 204, 2016 (doi).
D. S. Nogueira Nunes and M. Ayala-Rincón A Practical Semi-External Memory Method for Approximate Pattern Matching. ENTCS 324:107-122, 2016. (doi).
L.A. da Silveira, J.L. Soncco-Álvarez and M. Ayala-Rincón Parallel Memetic Genetic Algorithms for Sorting Unsigned Genomes by Translocations. PDF, C code, CeC 2016 (doi ).
M. Ayala-Rincón, M. Fernández and D. Nantes-Sobrinho Nominal Narrowing. Proc. FSCD 2016, LIPIcs vol. 52:11:1-11:17, 2016 (doi).

2015

L.A. da Silveira, J.L. Soncco-Álvarez, T.A. de Lima and M. Ayala-Rincón Memetic and Opposition-Based 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 73-85, 2016). (doi).
L.A. da Silveira, J.L. Soncco-Álvarez, T.A. de Lima and M. Ayala-Rincón Computing Translocation Distance by a Genetic Algorithm. PDF, C code, IEEE Xplore Proceedings CLEI 2015. (doi).
M. Ayala-Rincón, Tutorial on Formal Reasoning with PVS given in the Nat@logic Reasoning School 2015, Natal, Brazil, 31 August - 1 September 2015.
- Tutorial foils
- PVS exercises
A. Viso, E. Bonelli and M. Ayala-Rincón, Type Soundness for Path Polymorphism. Pre-proceedings LSFA 2015:3-18, 2015, ArXiv extended version. ENTCS 2016 (doi).
M. Ayala-Rincón, M. Fernández and A.C. Rocha-Oliveira, Completeness in PVS of a Nominal Unification Algorithm. Pre-proceedings LSFA 2015:19-34, 2015. ENTCS 2016 (doi).
A.C. Rocha-Oliveira, M. Ayala-Rincó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:27-32, 2015.
M. Ayala-Rincón, M. Fernández, M.J. Gabbay and A.C. Rocha-Oliveira Checking Overlaps of Nominal Rewriting Rules. Pre-proceedings LSFA 2015:199-2014, 2015. ENTCS 2016 (doi).
D. L. Ventura, F. Kamareddine and M. Ayala-Rincón, Explicit substitution calculi with de Bruijn indices and intersection type systems. Logic Journal of the IGPL 23(2): 295-340, 2015. (doi).
J.L. Soncco-Álvarez, G.M. Almeida, J. Becker and M. Ayala-Rincón, Parallelization of genetic algorithms for sorting permutations by reversals over biological data. Int. J. Hybrid Intell. Syst. 12(1): 53-64, 2015. (doi).

2014

F.L.C. de Moura, D. Kesner and M. Ayala-Rincón Metaconfluence of Calculi with Explicit Substitutions at a Distance, In Proc. 34th International Conference on Foundation of Software Technology and Theoretical Computer Science FST&TCS 2014, LIPIcs Vol. 29 (doi).
M. Ayala-Rincó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.
- Tutorial foils
- PVS exercises
A.B. Avelar, A.L. Galdino, F.L.C. de Moura and M. Ayala-Rincón, First-order unification in the PVS proof assistant, Logic Journal of the IGPL 22(5):758-789, 2014. (doi).
D. S. Nogueira Nunes and M. Ayala-Rincón A compressed suffix tree based implementation with low peak memory usage. ENTCS 302:73-94, 2014. (doi).
E. H. Haeusler, M. Ayala-Rincó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 202-213. (doi).
D. M. Muñoz, C. H. Llanos, L. dos Santos Coelho, M. Ayala-Rincón, Hardware opposition-based PSO applied to mobile robot controllers. Engineering Applications of Artificial Intelligence 28:64-77, 2014. (doi)
A.A. Almeida, J. Arias-Garcia, C. H. Llanos and M. Ayala-Rincón, Verification of Hardware Implementations through Correctness of Their Recursive Definitions in PVS. ACM Proceedings 27th SBCCI, 2014.
J. L. Soncco-Alvarez and M. Ayala-Rincó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. Ayala-Rincó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 166-174, 2013.
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, Full PVS Theory: version PVS 5.n, version PVS 6.0). Journal of Formalized Reasoning, 6(1):31-61, 2013.
J.L. Soncco-Álvarez, G.M. Almeida, J. Becker and M. Ayala-Rincó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. S. Nogueira Nunes and M. Ayala-Rincón A compressed suffix tree based implementation with low peak memory usage. Published in ENTCS CLEI 2013 (Symp. of Theory of Computation), Naiguatá, Venezuela.
T.A. de Lima and M. Ayala-Rincó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. Ayala-Rincó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 47-52, PVS tgz file), Eindhoven, Netherlands.
D.M. Muñoz-Arboleda, C. H. Llanos, L. Coelho and M. Ayala-Rincón, Hardware-based Parallel Firefly Algorithm for Embedded Applications, In IEEE Proc NASA/ESA Conference on Adaptive Hardware and Systems, (doi), 2013. Torino, Italy.
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). (doi), 2013, Cape Town, South Africa.

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. S. Nogueira Nunes 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))
F.L.C. de Moura, A.B. Barbosa and M. Ayala-Rincón A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi, (LSFA 2010) ENTCS 269:41-54, 2011 ((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) or (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)). 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 published 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