Books
Tutorials and Talks
- M. Ayala-Rincón Formalisation of nominal equational reasoning in PVS:
nominal Unification .
Talk (video), Workshop:
"Libraries of Digital Math", Hausdorff Trimester
Program: "Prospects of Formal Mathematics", HIM,
Universität Bonn, 2024.
- M. Ayala-Rincón Formalisation of nominal equational reasoning in PVS:
Anti-Unification
Talk (video), Hausdorff Trimester
Program: "Prospects of Formal Mathematics", HIM,
Universität Bonn, 2024.
- M. Ayala-Rincón Exemplifying
Formal Mathematics. Talk XVI Summer
Workshop in Mathematics, 2024.
- 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 15th 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 10th International School on Rewriting - ISR 2018,
Cali, Colombia, 30 July - 3 August 2018.
- 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.
- M. Ayala-Rincón, Invited Talk Formalising Confluence given in
the 11th Developments in Computational Models - DCM 2015 (satellite of the 12th 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 7th International School on Rewriting - ISR 2014,
Valparaíso Chile, 25 to 29 August 2014.
Publications by year
-
2024
- M. Ayala-Rincón, D. M. Cerna,
A. F. González Barragán, and T. Kutsia Equational Anti-Unification over Absorption Theories,
Proc. 12th International Joint Conference on Automated
Reasoning - IJCAR (IJCAR),
Springer (LNCS) LNAI 14740, pages 317-337, 2024.
- 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, Swarm and Evolutionary
Computation, vol. 89, paper 101624, 2024. (doi, Personalized Share Link)
- A. F. González Barragán, D. M. Cerna,
M. Ayala-Rincón, and T. Kutsia On Anti-Unification over Absorption, Associative, and
Commutative Theories,
Proc. 38th Int. Workshop on Unificaton UNIF (LTCS-Report
24-04 doi) Technische
Universität Dresden, pp. 56-61, 2024.
- Gabriela Ferreira, D. M. Cerna,
M. Ayala-Rincón, and T. Kutsia Computing Generalizers over Intersection and Union Type Theories,
Proc. 38th Int. Workshop on Unificaton UNIF (LTCS-Report
24-04 doi) Technische
Universität Dresden, pp. 62-68, 2024.
-
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.
Published in EPTCS 402:18-33, 2024. (doi)
- 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 10th International School on Rewriting - ISR 2018,
Cali, Colombia, 30 July - 3 August 2018.
- 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
-
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.
- 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. 29th 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 7th 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. 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 3rd 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 3rd 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. (doi)
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 15th 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).
- 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. 4th 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. 5th International Workshop on the Implementation of Logics held in conjunction with the Proc. 11th 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. 11th 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. 23rd SCCC, pp 60-69, 2003..
- M. Ayala-Rincón and F. Kamareddine, On Applying the lambda se-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).
.
- 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. 9th 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. 9th 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 se-Style of Unification for Simply-Typed Higher Order Unification in the Pure lambda Calculus, In Pre-Proceedings 8th 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 se-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 se-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 se-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 se-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