Mauricio Ayala Rincon
Possui graduação em "Ingeniería de Sistemas y Computación" (1985) e em "Matemáticas" (1987) da Universidad de Los Andes (Bogotá, Colômbia) e doutorado (Dr. rer. nat.) em Teoria da Computação (1993) da Fachbereich Informatik, Universität Kaiserslautern (Alemanha). Atualmente é Professor Titular em Ciência da Computação da Universidade de Brasília e pesquisador e consultor ad-hoc do Conselho Nacional de Desenvolvimento Científico e Tecnológico - CNPq. É membro do Corpo Editorial da Revista Colombiana de Computación, e foi editor convidado de números especiais de Journal of Automated Reasoning, Mathematical Structures in Computer Sciences, Theoretical Computer Science, J. of the IGPL e ENTCS. Foi pesquisador associado (1999-2000) e afiliado (2000-2010) do Grupo ULTRA da Heriot-Watt University (Edimburgo, U.K.) e, consultor do National Institute of Aerospace NIA/NASA LaRC entre Jul-Set 2010. Participou da criação do curso de Mestrado (2003) e coordenou a criação do curso de Doutorado (2010) em Informática da Universidade de Brasília. Tem experiência na área de Ciência da Computação, com ênfase em Teoria da Computação, atuando principalmente nos seguintes temas: teoria de reescrita, especificação algébrica, substituições explícitas, cálculo lambda, sistemas nominais, especificação de sistemas reconfiguráveis e métodos formais. As suas principais contribuições são no tratamento de sistemas de reescrita condicionais com predicados aritméticos, no desenvolvimento de mecanismos de unificação de ordem superior via cálculos de substituições explícitas e unificação nominal módulo, no desenvolvimento de uma metodologia baseada em reescrita-lógica para o projeto de hardware reconfigurável e, na formalização de propriedades de sistemas de reescrita e sistemas nominais. Foi co-organizador do Workshop on Logic, Language, Information and Computation WoLLIC em 2001, 2008 e 2010 e do Logical and Semantic Frameworks with Applications LSFA desde sua criação em 2006 até 2017, e a partir de 2022, sendo co-chair do PC deste último em 2006, 2007, 2009, 2014 e 2021. Foi eleito em 2007 "Conference Chair" da "Federated Conference on Rewriting, Deduction and Programming - RDP 2009" realizada em Brasília em junho/julho de 2009. RDP 2009 incluiu as conferências "9th Typed Lambda Calculus and Applications" e "20th Rewriting Techniques and Applications". Eleito em 2009, membro do Steering Committee da International School on Rewriting ISR (2009-15), sendo presidente deste SC entre 2014-2015 e, eleito em Nagoya 2012 membro do Steering Committee de Rewriting Techniques and Applications RTA (2012-15). Neste último comitê participou da criação da nova conferência Formal Structures for Computation and Deduction FSCD, que sucedeu RDP a partir de 2016, sendo eleito em Oxford 2018, membro do Steering Committee de FSCD (2018-21). Foi co-chair da conferência "8th Interactive Theorem Proving" (ITP 2017) e membro ex-officio do Steering Committee de ITP (2017-18), e foi nomeado membro do Steering Committee de ITP (2020-). Foi co-chair do "32nd International Workshop on Unification" (UNIF 2018) afiliado a FSCD/FLOC 2018 e dos "8th" e "9th" International Workshops on Confluence" (IWC 2019, IWC 2020) afiliados a FSCD 2019 e FSCD/IJCAR 2020. Foi nomeado co-chair do Steering Committee de IWC em 2020. Foi nomeado em 2021, membro do IFIP working group 1.6: rewriting. Atualmente, é Conference Chair da 18th Conference on Computational Intelligent Mathematics, colocada com o 20th Logical and Semantic Frameworks with Applications (CICM+LSFA 2025), a ser realizada em Brasília entre 6-11 Novembro de 2025.
Informações coletadas do Lattes em 13/08/2025
Acadêmico
Formação acadêmica
Doutorado em Fachbereich Informatik
1989 - 1993
Universitaet Kaiserslautern
Título: Expressiveness of Conditional Rewriting Systems with Built-in Predicates
Orientador: Prof Dr. rer. nat. Klaus Erwin Madlener
Bolsista do(a): Deutscher Akademischer Austauschdienst, DAAD, Alemanha. Palavras-chave: Especificacao Algebrica; Prova de Teoremas; Sistemas de Reescrita de Termos.Grande área: Ciências Exatas e da Terra
Graduação em Matemática
1981 - 1987
Universidad de Los Andes
Título: Algunos Aspectos de la Teoria de Bifurcaciones
Orientador: Prof Dr. rer. nat. Jaime Lesmes
Graduação em Ingeniería de Sistemas y Computación
1980 - 1985
Universidad de Los Andes
Título: Generador de Evaluadores para Gramáticas con Atributos Fuertemente No-Circulares
Orientador: Prof Dr. Rodrigo Lopez
Pós-doutorado
2024 - 2025
Pós-Doutorado. , Research Institute for Symbolic Computation / Johannes Kepler Universität, RISC/JKU, Austria. , Bolsista do(a): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior, CAPES, Brasil. , Grande área: Ciências Exatas e da Terra, Grande Área: Ciências Exatas e da Terra / Área: Matemática / Subárea: Álgebra / Especialidade: Lógica Matemática. , Grande Área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação / Especialidade: Análise de Algoritmos e Complexidade de Computação.
1999 - 2000
Pós-Doutorado. , Heriot-Watt University, HWU, Grã-Bretanha. , Bolsista do(a): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior, CAPES, Brasil. , Grande área: Ciências Exatas e da Terra, Grande Área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação / Especialidade: Computabilidade e Modelos de Computação.
1994 - 1994
Pós-Doutorado. , Universidade de Brasília, UnB, Brasil. , Bolsista do(a): Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPq, Brasil. , Grande área: Ciências Exatas e da Terra, Grande Área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação. , Grande Área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação / Especialidade: Análise de Algoritmos e Complexidade de Computação.
Idiomas
Inglês
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.
Espanhol
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.
Português
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.
Alemão
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.
Áreas de atuação
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação.
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação/Especialidade: Lógicas e Semântica de Programas.
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação/Especialidade: Computabilidade e Modelos de Computação.
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação/Especialidade: Análise de Algoritmos e Complexidade de Computação.
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação/Especialidade: Linguagem Formais e Autômatos.
Grande área: Ciências Exatas e da Terra / Área: Matemática / Subárea: Matemática Aplicada.
Organização de eventos
Ayala-Rincón, Mauricio ; de PAIVA, V. ; KOEPKE, P. ; NALON, Cláudia ; FINGER, M. ; De Lima, T.A. ; HAEUSLER, Edward Herman ; MOURA, Flávio Leonardo Cavalcanti de ; Avelar, Andréia B ; GALDINO, André ; VENTURA, Daniel Lima ; SZASZ, Nora ; Rocha, C. ; Díaz-Caro, A. . Conference Chair 18th Congress on Intelligent Computer Mathematics - CICM 2025. 2024. (Congresso).
M. Ayala-Rincón . Steering Committee Member - 15th International Conference on Interactive Theorem Proving ITP. 2024. (Congresso).
Winkler, S. ; M. Ayala-Rincón . Steering Committee co-chair - 13th International Workshop on Conlfuence. 2024. (Congresso).
M. Ayala-Rincón ; NALON, Cláudia ; MOURA, Flávio Leonardo Cavalcanti de ; Avelar, Andréia B ; VENTURA, Daniel Lima ; De Lima, T.A. ; GALDINO, André ; Barbosa, H. ; Ringeissen, C. . Conference Chair - 20th Logical and Semantic Frameworks, with Applications - LSFA 2025. 2024. (Congresso).
Ayala-Rincón, Mauricio . Steering Committee Member - 14th International Conference on Interactive Theorem Proving ITP. 2023. (Congresso).
Ayala-Rincón, Mauricio ; Aotho, Takahito . Steering Committee co-chair - 12th International Workshop on Conlfuence. 2023. (Congresso).
Paulson, L. ; Blanchette, J. ; Bertot, Y. ; Mahboubi, A. ; M. Ayala-Rincón ; Klein, G. ; Myreen, M. ; Slobodova, A. ; Commelin, J. ; Kaliszyk, C. ; Cohen, L. ; Andronick, J. ; Naumowicz, A. . Steering Committee Member - 13th International Conference on Interactive Theorem Proving ITP 2022. 2022. (Congresso).
Giraldi, Silvio ; Schmidt-Schauss, M ; Gascón, Adrià ; Lynch, Christopher ; Balbiani, Philippe ; Erbatur, Serdar ; Sobrinho, Daniele Nantes ; M. Ayala-Rincón . Steering Committee Member - 36th International Workshop on Unification UNIF 2022. 2022. (Congresso).
Aotho, Takahito ; M. Ayala-Rincón . Steering Commitee co-Chair 11th International Workshop on Confluence. 2022. (Congresso).
KESNER, Delia ; Ayala-Rincón, Mauricio . Steering Committee Member - International Conference on Formal Structures for Computation and Deduction FSCD 2021. 2021. (Congresso).
Aotho, Takahito ; Ayala-Rincón, Mauricio . Steering Commitee co-Chair 10th International Workshop on Confluence. 2021. (Congresso).
Paulson, L. ; M. Ayala-Rincón ; Blanchette, J. ; URBAN, C. ; Mahboubi, A. ; Klein, G. ; Myreen, M. ; Manolios, P. ; Bertot, Y. . Steering Committee Member - 12th International Conference on Interactive Theorem Proving ITP 2021. 2021. (Congresso).
Ayala-Rincón, Mauricio ; Schmidt-Schauss, M ; NANTES-SOBRINHO, DANIELE ; Erbatur, Serdar ; Balbiani, Philippe ; Giraldi, Silvio ; Gascón, Adrià ; Lynch, Christopher . Steering Committee Member - 35th International Workshop on Unification UNIF 2021. 2021. (Congresso).
Schmidt-Schauss, M ; AYALA-RINCON, MAURICIO ; Kutsia, T. ; Sobrinho, Daniele Nantes ; Giraldi, Silvio ; Erbatur, Serdar ; Kennedy, Andrew ; Lynch, Christopher ; Gascón, Adrià ; Balbiani, Philippe . Steering Committee Member - 34th International Workshop on Unification UNIF 2020, Paris. 2020. (Congresso).
KESNER, Delia ; AYALA-RINCON, MAURICIO . Steering Committee Member - International Conference on Formal Structures for Computation and Deduction FSCD 2020. 2020. (Congresso).
Aotho, Takahito ; AYALA-RINCON, MAURICIO . Steering Commitee co-Chair 9th International Workshop on Confluence. 2020. (Congresso).
Paulson, L. ; Manolios, P. ; URBAN, C. ; Blanchette, J. ; Myreen, M. ; Klein, G. ; Mahboubi, A. ; Ayala-Rincon, M. . Steering Committee Member - 11th International Conference on Interactive Theorem Proving ITP. 2020. (Congresso).
M. Ayala-Rincón ; KESNER, Delia . Steering Committee Member - International Conference on Formal Structures for Computation and Deduction FSCD 2019. 2019. (Congresso).
Schmidt-Schauss, M ; M. Ayala-Rincón ; Balbiani, Philippe ; Giraldi, Silvio ; Gascón, Adrià ; Lynch, Christopher ; Erbatur, Serdar ; Sobrinho, Daniele Nantes . Steering Committee Member - 33rd International Workshop on Unification, UNIF 2019. 2019. (Congresso).
M. Ayala-Rincón . Steering Committee Member Ex Officio - International Conference on Interactive Theorem Proving ITP 2018. 2018. (Congresso).
M. Ayala-Rincón ; KESNER, Delia . Steering Committee Member - International Conference on Formal Structures for Computation and Deduction FSCD 2018. 2018. (Congresso).
Escobar, Santiago ; M. Ayala-Rincón ; Vilaret, Mateu ; Giraldi, Silvio ; Lynch, Christopher ; Gascón, Adrià ; Balbiani, Philippe ; Schmidt-Schauss, M . Steering Committee Member - 32nd International Workshop on Unification UNIF 2018. 2018. (Congresso).
Ayala-Rincón, Mauricio ; Rose, K. ; Dowek, G. ; Stump, A. ; Tison, Sophie ; Hirokawa, Nao . Steering Committee member - 26th International Conference on Rewriting Techniques and Applications -RTA 2015. 2015. (Congresso).
Ayala-Rincón, Mauricio ; Castro, C. ; Waldmann, Johannes ; Keller, Gabriele ; OOSTROM, V. V. . Steering Committee member - Eighth International School on Rewriting -ISR 2015. 2015. (Outro).
Castro, C. ; KIRCHNER, C. ; Lucas, Salvador ; M. Ayala-Rincón ; Middeldorp, Aart ; OOSTROM, V. V. . Steering Committee member - Seventh International School on Rewriting -ISR 2014. 2014. (Outro).
Moser, G. ; Dowek, G. ; Stump, A. ; Rose, K. ; M. Ayala-Rincón ; Tison, Sophie . Steering Committee member - 25th International Conference on Rewriting Techniques and Applications - RTA 2014. 2014. (Congresso).
M. Ayala-Rincón ; Moser, G. ; Lucas, Salvador ; Blanqui, Fréderic ; Tison, Sophie ; Sakai, Masahiko . Steering Committee member - 24th International Conference on Rewriting Techniques and Applications -RTA 2013. 2013. (Congresso).
M. Ayala-Rincón ; FINGER, Marcelo ; FERNANDEZ, M. ; WASSERMANN, R. . OC member - Eighth Workshop on Logical and Semantic Frameworks, with Applications - LSFA 2013. 2013. (Congresso).
Ayala-Rincon, M. ; Giesl, Juergen ; KIRCHNER, C. ; Lucas, Salvador ; Middeldorp, Aart ; OOSTROM, V. V. . Steering Committee member - Sixth International School on Rewriting -ISR 2012. 2012. (Outro).
FREITAS, R. ; BRAGA, Christiano ; PEREIRA, Luiz Carlos P D ; Ayala-Rincon, M. . OC co-chair - Seventh Workshop on Logical and Semantic Frameworks, with Applications - LSFA 2012. 2012. (Congresso).
Ayala-Rincon, M. . Publication Chair - 25th Symposium on Integrated Circuits and Systems Design - SBCCI 2012. 2012. (Congresso).
PIMENTEL, E. ; Della Rocca, Simona Ronchi ; Ayala-Rincon, M. ; HAEUSLER, Edward Herman . OC member - Sixth Workshop on Logical and Semantic Frameworks, with Applications - LSFA 2011. 2011. (Congresso).
AYALARINCON, M ; QUEIROZ, R. G. ; MOURA, Flávio Leonardo Cavalcanti de ; NALON, Cláudia . OC Chair - Workshop on Logic, Language, Information and Computation - WoLLIC 2010. 2010. (Congresso).
KIRCHNER, C. ; Middeldorp, Aart ; Ayala-Rincon, M. ; OOSTROM, V. V. . Steering Committee member - Fifth International School on Rewriting - ISR 2010. 2010. (Outro).
TREINEN, R. ; CURIEN, P. ; M. Ayala-Rincón . Conference Chair - Federated Conference on Rewriting, Deduction, and Programming, RDP 2009. 2009. (Congresso).
AYALARINCON, M ; MOURA, Flávio Leonardo Cavalcanti de . Organising co-Chair - Fourth International School on Rewriting - ISR 2009. 2009. (Outro).
NALON, Cláudia ; PIMENTEL, E. ; PINTO, G. A. ; M. Ayala-Rincón ; HAEUSLER, Edward Hermann . OC member - Fourth Workshop on Logical and Semantic Frameworks, with Applications - LSFA 2009. 2009. (Congresso).
Ayala-Rincon, M. ; TREINEN, R. . OC chair - 20th International Conference on Rewriting Techiques and Applications -RTA 2009. 2009. (Congresso).
PIMENTEL, E. ; BENEVIDES, M. ; M. Ayala-Rincón ; HAEUSLER, Edward Hermann . OC member - Third Wokrshop on Logical and Semantic Frameworks, with Applications - LSFA 2008. 2008. (Congresso).
QUEIROZ, R. G. ; KAMAREDDINE, Fairouz ; M. Ayala-Rincón ; HODGES, W. . OC member - Workshop on Logic, Language, Information and Computation - WoLLIC 2008. 2008. (Congresso).
M. Ayala-Rincón ; HAEUSLER, Edward Hermann . OC member - Second Wokrshop on Logical and Semantic Frameworks, with Applications - LSFA 2007. 2007. (Congresso).
BRAGA, Christiano ; M. Ayala-Rincón ; HAEUSLER, Edward Hermann . OC co-chair - Wokrshop on Logical and Semantic Frameworks, with Applications - LSFA 2006. 2006. (Congresso).
QUEIROZ, R. G. ; M. Ayala-Rincón ; HAEUSLER, Edward Hermann . OC Chair - Workshop on Logic, Language, Information and Computation - WoLLIC 2001. 2001. (Congresso).
Participação em eventos
10th International Conference on Formal Structures for Computation and Deduction _ FSCD 2025. PC member FSCD 2025. 2025. (Congresso).
17th NASA Formal Methods Symposium (NFM 2025). PC member NFM 2025. 2025. (Congresso).
19th Logical Frameworks and Meta-languages: Theory and Practice.PC member LFMTP 2024. 2024. (Oficina).
26th International Conference on Foundations of Software Science and Computation Structures FoSSaCS. PC member FoSSaCS 2024. 2024. (Congresso).
5o Workshop Brasileiro de Lógica.PC co-chair. 2024. (Oficina).
9th International Conference on Formal Structures for Computation and Deduction - FSCD 2024. PC member FSCD 2024. 2024. (Congresso).
IEEE Congress on Evolutionary Computation CEC 2024. PC reviewer CEC 2024. 2024. (Congresso).
The 38th International Workshop on Unification UNIF 2024. PC member UNIF 2024. 2024. (Congresso).
The fifteenth International Conference on Interactive Theorem Proving (ITP 2024). PC member ITP 2024. 2024. (Congresso).
18th Logical and Semantic Framework with applications. PC member LSFA 2023. 2023. (Congresso).
37th International Workshop on Unification UNIF 2023. PC member UNIF 2023. 2023. (Congresso).
Fourteenth conference on Interactive Theorem Proving ITP 2023. PC member ITP 2023. 2023. (Congresso).
IEEE Congress on Evolutionary Computation CEC 2023. PC reviewer CEC 2023. 2023. (Congresso).
The 16th Conference on Intelligent Computer Mathematics. CICM 2023. PC member CICM 2023. 2023. (Congresso).
17th Logical and Semantic Framework with applications LSFA 2022. PC member LSFA 2022. 2022. (Congresso).
36th International Workshop on Unification UNIF 2022. PC member UNIF 2022. 2022. (Congresso).
IEEE Congress on Evolutionary Computation CEC 2022. PC reviewer CEC 2022. 2022. (Congresso).
The 11th ACM SIGPLAN International Conference on Certified Programs and Proofs CPP 2022.. PC member CPP 2022 - afiliado a POPL. 2022. (Congresso).
13th NASA Formal Methods Symposium - NFM 2021. PC Member NFM 2021. 2021. (Congresso).
2o Workshop Brasileiro de Lógica (WBL).Membro do CP WBL 2021 - parte do CSBC 2021. 2021. (Oficina).
35th International Workshop on Unification UNIF 2021. PC member 35th Int. Workshop on Unification. 2021. (Congresso).
5th workshop on Formal Mathematics for Mathematicians (FFM 2021).PC Member 5th workshop on Formal Mathematics for Mathematicians - Colocado com 14th CICM. 2021. (Oficina).
IEEE Congress on Evolutionary Computation CEC 2021. Reviewer CeC 2021. 2021. (Congresso).
International Conference on Formal Structures for Computation and Deduction FSCD 2021. PC member FSCD 2021. 2021. (Congresso).
PC co-chair 16th Logical and Semantic Frameworks with Applications. PC co-chair 16th LSFA a ser afiliado a FSCD 2021. 2021. (Congresso).
The 14th Conference on Intelligent Computer Mathematics (CICM 2021). PC member 14th Conference on Intelligent Computer Mathematics. 2021. (Congresso).
15th Logical and Semantic Frameworks with Applications. Invited Speaker LSFA. 2020. (Congresso).
1o Workshop Brasileiro de Lógica (WBL).PC member 1o WBL. 2020. (Oficina).
30th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2020). PC Member LOPSTR 2020. 2020. (Congresso).
34th International Workshop on Unification UNIF 2020 - part of IJCAR-FSCD. PC Member UNIF 2020. 2020. (Congresso).
Co-chair International Workshop on Confluence IWC 2020. Co-chair Comitê de Programa do IWC 2020 (Samuel Miriam e M. Ayala-Rincón). 2020. (Congresso).
IEEE Congress on Evolutionary Computation CEC 2020. Reviewer CeC 2020. 2020. (Congresso).
The 9th ACM SIGPLAN International Conference on Certified Programs and Proofs CPP 2020. PC member CPP 2020 - Afiliada a POPL. 2020. (Congresso).
10th Southern Programmable Logic Conference SPL 2019. PC Member SPL 2019. 2019. (Congresso).
19th Brazilian Logic Conference EBL 2019. PC Member EBL 2019. 2019. (Congresso).
33nd International Workshop on Unification UNIF 2019 - part of FSCD. PC member UNIF 2019 - Part of FSCD. 2019. (Congresso).
8th ACM SIGPLAN International Conference on Certified Programs and Proofs CPP 2019. PC member CPP 2019 - Afiliada a POPL. 2019. (Congresso).
Co-chair 8th International Workshop on Confluence IWC 2019. co-chair Comitê de Programa do IWC 2019 (Jakob Grue Simonsen e M. Ayala-Rincón). 2019. (Congresso).
IEEE Congress on Evolutionary Computation CEC 2019. Reviewer CeC 2019. 2019. (Congresso).
International Conference on Formal Structures for Computation and Deduction FSCD 2019. PC member FSCD 2019. 2019. (Congresso).
Tenth International Conference Interative Theorem Proving ITP 2019. PC member IP 2019. 2019. (Congresso).
XLV Conferencia Latinoamericana de Informática CLEI - SLTC 2019. PC member of CLEI - Simposio Latinoamericano de Teoría Computacional. 2019. (Congresso).
13 Congreso Colombiano de Computación - 13CCC. PC member 13o Congreso Colombiano de Computación - 13CCC. 2018. (Congresso).
13th Logical and Semantic Frameworks with Applications LSFA 2018. PC member 13th LSFA 2018. 2018. (Congresso).
Co-chair 32nd International Workshop on Unification UNIF 2018 - part of FSCD/FLoC. PC chair UNIF 2018 - Colocado con FSCD/FLoC 2018. 2018. (Congresso).
IEEE Congress on Evolutionary Computing CeC 2018. PC Reviewer CeC 2018. 2018. (Congresso).
Tenth NASA Formal Methods Symposium - NFM 2018. PC member Tenth NASA Formal Methods - NFM 2018. 2018. (Congresso).
XLIV CLEI / SLTC Simpósio Latino-Americano em Teoria Computacional.PC member XLIV CLEI / SLTC. 2018. (Simpósio).
12 Congreso Colombiano de Computación 12CCC. PC member 12o Congreso Colombiano de Computación - 12CCC. 2017. (Congresso).
17th International Conference on Intelligent Systems Design and Applications (ISDA 2017). PC member ISDA 2017. 2017. (Congresso).
18th Brazilian Logic Conference (EBL 2017). PC Member EBL 2017. 2017. (Congresso).
Co-chair Eighth International Conference Interative Theorem Proving ITP 2017. PC co-chair 8th ITP 2017. 2017. (Congresso).
Eleventh International Symposium on Frontiers of Combining Systems FroCoS 2017.PC member 11th FroCos 2017. 2017. (Simpósio).
IEEE Congress on Evolutionary Computation CeC 2017. PC reviewer CeC 2017. 2017. (Congresso).
Twelfth Logical and Semantic Frameworks with Applications- LSFA 2017. PC member 12th LSFA 2017. 2017. (Congresso).
11 Congreso Colombiano de Computación - 11CCC. PC member 11o Congreso Colombiano de Computación - 11CCC. 2016. (Congresso).
13th International Colloquium on Theoretical Aspects of Computing - ICTAC 2016. PC member 13th ICTAC 2016. 2016. (Congresso).
16th International Conference on Intelligent Systems Design and Applications (ISDA). PC member 16th ISDA 2016. 2016. (Congresso).
8th World Congress on Nature and Biologically Inspired Computing (NaBiC 2016 h. PC member 8th NaBIC 2016. 2016. (Congresso).
Eleventh Logical and Semantic Frameworks with Applications- LSFA 2016. PC member 11th LSFA 2016. 2016. (Congresso).
IEEE Congress on Evolutionary Computation CeC 2016. PC reviewer CeC 2016. 2016. (Congresso).
12th International Colloquium on Theoretical Aspects of Computing - ICTAC 2015. PC member 12th ICTAC 2015. 2015. (Congresso).
26th International Conference on Rewriting Techniques and Applications RTA 2015. PC member 26th RTA 2015. 2015. (Congresso).
28th Symposium on Integrated Circuits and Systems Design - SBCCI 2015. PC member 28th SBCCI. 2015. (Congresso).
4th International Workshop on Confluence - IWC 2015. PC member IWC 2015. 2015. (Congresso).
7th World Congress on Nature and Biologically Inspired Computing (NaBiC 2015 h. PC member 7th World Congress on Nature and Biologically Inspired Computing. 2015. (Congresso).
Décimo Congreso Colombiano de Computación - 10CCC. Membro do Comitê Científico do Décimo Congreso Colombiano de Computación - 10CCC. 2015. (Congresso).
Developments in Computational Models DCM 2015 / ICTAC 2015. Invited talk: Formalising Confluence. 2015. (Congresso).
IEEE Congress on Evolutionary Computation CeC 2015. PC reviewer CeC 2015. 2015. (Congresso).
International Joint Conference on Artificial Intelligence (IJCAI'15). Senior PC member IJCAI 2015. 2015. (Congresso).
Nat@Logic - TRS School on Reasoning.Invited Lecturer - Formal Reasoning with PVS - 4h short-course. 2015. (Oficina).
Tenth Logical and Semantic Frameworks, with Applications - LSFA 2015. Membro do Comitê Científico do 10th Logical and Semantic Frameworks with Applications - LSFA 2015. 2015. (Congresso).
14th International Conference on Intelligent Systems Design and Applications (ISDA). PC member 14th International Conference on Intelligent Systems Design and Applications (ISDA). 2014. (Congresso).
17th Brazilian Logic Conference (EBL 2014). PC member 17th EBL. 2014. (Congresso).
23rd International Workshop on Functional and (Constraint) Logic Programming WFLP. PC member 23rd International Workshop on Functional and (Constraint) Logic Programming - WFLP. 2014. (Congresso).
27th Symposium on Integrated Circuits and Systems Design - SBCCI 2014.PC member 27th SBCCI. 2014. (Simpósio).
4th World Congress on Information and Communication Technologies WCIT 2014. PC member 4th World Congress on Information and Communication Technologies. 2014. (Congresso).
6th World Congress on Nature and Biologically Inspired Computing (NaBiC 2014. PC member 6th World Congress on Nature and Biologically Inspired Computing. 2014. (Congresso).
7th International School on Rewriting (ISR 2014). Invited Lecturer - Formalisation in PVS of Rewriting Properties - 6h Mini-course. 2014. (Congresso).
Co-chair Ninth Logical and Semantic Frameworks, with Applications - LSFA 2014. Co-chair do Comitê Científico (Ian Mackie e M. Ayala-Rincon). 2014. (Congresso).
Concurso de Teses e Dissertações - CTD 2014 (Congresso da SBC 2014). Miembro do Comitê Avaliador CTD-SBC 2014. 2014. (Congresso).
IEEE Congress on Evolutionary Computation CeC 2014. PC reviewer CeC 2014. 2014. (Congresso).
IX Southern Programmable Logic Conference SPL. Membro do Comitê Científico do SPL2014. 2014. (Congresso).
Noveno Congreso Colombiano de Computación - 9CCC. Membro do Comitê Científico do Noveno Congreso Colombiano de Computación - 9CCC. 2014. (Congresso).
PhD forum - IEEE CS Annual Symposium on VLSI. Membro do Comitê Julgador do PhD forum do 2014 ISVLSI. 2014. (Congresso).
The Fifth International Symposium on Innovations in Information & Communications Technology (ISIICT 2014). PC member ISIICT 2014. 2014. (Congresso).
2013 8th Computing Colombian Conference (8CCC). Tutorial Convidado: Computational Deduction and Formal Proofs Logic for Computation that is truly Computational. and PC member. 2013. (Congresso).
26th Symposium on Integrated Circuits and Systems Design - SBCCI 2013.PC member 26th SBCCI. 2013. (Simpósio).
3rd World Congress on Information and Communication Technologies WCIT 2013. Membro do Comitê Científico do 3rd World Congress on Information and Communication Technologies WCIT 2013. 2013. (Congresso).
5th World Congress on Nature and Biologically Inspired Computing (NaBiC 2013). PC member 5th World Congress on Nature and Biologically Inspired Computing. 2013. (Congresso).
Co-chair 9th International Workshop on Developments in Computational Models. PC co-chair DCM 2013 9th International Workshop on Developments in Computational Models. 2013. (Congresso).
Eighth Logical and Semantic Frameworks, with Applications - LSFA 2013.Membro do Comitê Científico do 8th LSFA. 2013. (Simpósio).
IEEE Congress on Evolutionary Computation CeC 2013. PC reviewer CeC 2013. 2013. (Congresso).
PhD forum - IEEE CS Annual Symposium on VLSI. Membro do Comitê Julgador do PhD forum do 2013 ISVLSI. 2013. (Congresso).
2012 7th Colombian Computing Congress (7CCC). Membro do Comitê Científico do Séptimo Congreso Colombiano de Computación - 7CCC. 2012. (Congresso).
25th Symposium on Integrated Circuits and Systems Design - SBCCI 2012.PC member 25th SBCCI. 2012. (Simpósio).
Concurso de Trabalhos de Iniciação Científica (SBC 2012). Membro do Comitê do Programa do Concurso de Trabalhos de Iniciação Científica CTIC - XXXI - SBC 2012. 2012. (Congresso).
IEEE Congress on Evolutionary Computation CeC 2012. PC reviewer CeC 2012. 2012. (Congresso).
International Symposium on Symbolic Computation in Software Science - SCSS 2012.Membro do Comitê do Programa Int. Symp. on Symbolic Computation in Software Sciences SCSS 2012. 2012. (Simpósio).
IV Simpósio de Matemática Industrial SIMMI.Palestra convidada: Reuso de Demonstrações Formais em PVS. 2012. (Simpósio).
Latin American Congress on Requirements Engineerings & Software Testing LACREST. Palestra convidada: Reusing Formal Proofs Through Isomorophisms. 2012. (Congresso).
PhD forum - IEEE CS Annual Symposium on VLSI. Membro do Comitê Julgador do PhD forum do 2012 ISVLSI. 2012. (Congresso).
Seventh Logical and Semantic Frameworks, with Applications - LSFA 2012.Membro do Comitê Científico do 7th LSFA. 2012. (Simpósio).
VIII Southern Programable Logic Conference SPL. Membro do Comitê Científico. 2012. (Congresso).
2011 6th Colombian Computing Congress (6CCC). Palestra convidada: Aplicação de Técnicas Formais para Verificação e Automação de Propriedades de Sisteas Computacionais. 2011. (Congresso).
21st International Conference on Field Programable Logic and Applications FPL 2011. Membro do Comitê Científico. 2011. (Congresso).
24rd Symposium on Integrated Circuits and Systems Design - SBCCI 2011.Membro do Comitê do Programa SBCCI 2011. 2011. (Simpósio).
PhD forum IEEE CS annual Symposium on VLSI.Membro do Comitê do Programa do ISVLSI 2010 PhD Forum. 2011. (Simpósio).
Sixth Logical and Semantic Frameworks, with Applications - LSFA 2011.Membro do Comitê do Programa LSFA 2011. 2011. (Simpósio).
20th International Conference on Field Programable Logic and Applications FPL 2010. Membro do Comitê Científico. 2010. (Congresso).
23rd Symposium on Integrated Circuits and Systems Design - SBCCI 2010.Membro do Comitê de Programa SBCCI 2010. 2010. (Simpósio).
Fifth Logical and Semantic Frameworks, with Applications - LSFA 2010. Membro do Comitê de Programa LSFA 2010. 2010. (Congresso).
PhD forum IEEE CS annual Symposium on VLSI. Membro do Comitê de Programa PhD Forum ISVLSI 2010. 2010. (Congresso).
Quinto Congreso Colombiano de Computación - 5CCC. Membro do Comitê de Programa V CCC 2010. 2010. (Congresso).
Reconfigurable Communication-centric Systems on Chip - ReCoSoC 2010. Palestra convidada: Automatizing the verification of the termination property of algorithms and processes. 2010. (Congresso).
SEMISH - XXXVII Seminário Integrado de Software e Hardware.Membro do Comitê de Programa SEMISH 2010. 2010. (Seminário).
19th International Conference on Field Programmable Logic and Applications - FPL 2009. Membro do Comitê Científico. 2009. (Congresso).
22nd Symposium on Integrated Circuits and Systems Design - SBCCI 2009.Membro do Comitê de Programa SBCCI 2009. 2009. (Simpósio).
9th International Workshop on Reduction Strategies in Rewriting and Programming - WRS 2009. Membro do Comitê Científico do 9th WRS 2009. 2009. (Congresso).
Co-chair Fourth Logical and Semantic Frameworks, with Applications - LSFA 2009. Co-chair Comitê de Programa do LSFA 2009. 2009. (Congresso).
Cuarto Congreso Colombiano de Computación - 4CCC. Palestra convidada: Rewriting, Types, Proofs and Veried Software & Hardware. 2009. (Congresso).
II Encuentro de Investigación de la Facultad de Ingeniería y Ciencias Básicas - Politécnico Grancolombiano.Palestra convidada: Formalisation of the Security of Cryptographyc Protocols: the Dolev-Yao Model. 2009. (Encontro).
I Simpósio de Matemática Industrial SIMMI.Palestra convidada: Rewriting Theory, Type Theory, Proof Theory and Verification. 2009. (Simpósio).
VI Congreso Internacional de semilleros de investigación. Palestra convidada: Reescritura y Formalización de Software & Hardware - Oportunidades de investigación en Brasília. 2009. (Congresso).
XVII Colombian Congress of Mathematics - CCM 2009. Mini-curso de seis horas convidado: Cálculos de Sustituciones explícitas con sistemas de tipos y aplicaciones en programación y demostración. 2009. (Congresso).
18th International Conference on Field Programmable Logic and Applications - FPL 2008. Membro do Comitê Científico. 2008. (Congresso).
21st Symposium on Integrated Circuits and Systems Design - SBCCI 2008. Membro do Comitê de Programa SBCCI 2008. 2008. (Congresso).
Tercer Congreso Colombiano de Computación - 3CCC. Membro do Comitê de Programa do 3ro Congresso da Sociedad Colombiana de Computación - CCC 2008. 2008. (Congresso).
The 3rd International Workshop on Reconfigurable Computing Education - RC education 2008. Membro do Comitê de Programa do 3rd International Workshop on Reconfigurable Computing Education. 2008. (Congresso).
Third Wokrshop on Logical and Semantic Frameworks, with Applications - LSFA 2008. Membro do Comitê Científico. 2008. (Congresso).
14th Reconfigurable Architectures Workshop RAW 2007. Membro do Comitê Científico. 2007. (Congresso).
17th International Conference on Field Programmable Logic and Applications - FPL 2007. Membro do Comitê Científico. 2007. (Congresso).
20th Symposium on Integrated Circuits and Systems Design - SBCCI 2007. Membro do Comitê Científico. 2007. (Congresso).
Co-chair Second Wokrshop on Logical and Semantic Frameworks, with Applications - LSFA 2007. Co-chair Comitê de Programa do LSFA 2007. 2007. (Congresso).
Regional Meeting on Reconfigurable Computing RMRC.Membro do Comitê de Programa, Regional Meeting on Reconfigurable Computing RMRC. 2007. (Encontro).
Segundo Congreso Colombiano de Computación - 2CCC. Palestra convidada: ?Sustituciones Explícitas en la Implementación de Ambientes Computacionales? Palestrante Convidado e Membro do Comitê de Programa do 2do Congresso da Sociedad Colombiana de Computación - CCC 2007. 2007. (Congresso).
Terceiro Simpósio de Ensino, Pesquisa e Extensão da UFG III SEPEC.Palestra convidada: ?Especificação e Verificação de Sistemas Computacionais? Palestrante convidado III SEPEC UFG Campus Catalão. 2007. (Simpósio).
The 2nd International Workshop on Reconfigurable Computing Education - RC education 2007. Membro do Comitê de Programa do 2nd International Workshop on Reconfigurable Computing Education. 2007. (Congresso).
XXXIII Conferencia Latinoamericana de Informática - CLEI 2007. Membro do Comitê Científico. 2007. (Congresso).
19th Symposium on Integrated Circuits and Systems Design - SBCCI 2005. Membro do Comitê de Programa SBCCI 2006. 2006. (Congresso).
Co-chair Wokrshop on Logical and Semantic Frameworks, with Applications - LSFA 2006. Co-chair Comitê de Programa do LSFA 2006. 2006. (Congresso).
The 1st International Workshop on Reconfigurable Computing Education - RC education 2006. Membro do Comitê de Programa do International Workshop on Reconfigurable Computing Education. 2006. (Congresso).
Workshop on High Performance Computing in the Life Sciences HPC LIFE. Membro do Comitê de Programa, Workshop on High Performance Computing in the Life Sciences. 2006. (Congresso).
XXXI Conferencia Latinoamericana de Informática - CLEI 2005. Membro do Comitê de Programa CLEI 2005. 2005. (Congresso).
Concurso de Teses e Dissertações - CTD 2004 (Congresso da SBC 2004).Membro do Comitê de Programa CDT/SBC 2004. 2004. (Outra).
5th Latin American Symposium on Theoretical Informatic LATIN 2002. Membro do Comitê de Programa LATIN 2002. 2002. (Congresso).
Thirty Five years of Automath. Membro do Comitê de Programa 35 years of Automath. 2002. (Congresso).
Workshop on Logic, Language, Information and Computation - WoLLIC 2002. Membro do Comitê de Programa WoLLIC 2002. 2002. (Congresso).
Segundo Encontro de Matemática Aplicada e Computacional em Brasília.Coordenador da área de Teoria da Computação: Segundo Encontro de Matemática Aplicada e Computacional em Brasília - SBMAC. 2001. (Encontro).
V Encontro de Matemática e Estatística do IME/UFG.Palestra convidada: ?Cálculos de Substituições Explícitas e Aplicações Computacionais? Palestrante convidado. 2001. (Encontro).
Festival Workshop in Foundations and Computations.Session Chair: Festival Workshop in Foundations and Computations. 2000. (Outra).
Participação em bancas
Sobrinho, Daniele NantesVENTURA, Daniel LimaM. Ayala-Rincón. Nominal Commutative Narrowing. 2022. Dissertação (Mestrado em Matemática) - Universidade de Brasília.
Sobrinho, Daniele NantesVENTURA, Daniel LimaM. Ayala-Rincón. Syntactic, Commutative and Associative Anti-Unification. 2022. Dissertação (Mestrado em Matemática) - Universidade de Brasília.
Sobrinho, Daniele Nantes; Alves, Sandra; DE LIMA, THAYNARA A.;Ayala-Rincon, M.. Operadores de Redução para Sistemas de Reescrita. 2021. Dissertação (Mestrado em Matemática) - Universidade de Brasília.
Sobrinho, Daniele NantesAyala-Rincon, M.VENTURA, Daniel Lima. Desunificação Nominal via Restrições de Ponto Fixo. 2021. Dissertação (Mestrado em Matemática) - Universidade de Brasília.
JACOBI, Ricardo P; Pfenning, Franz;M. Ayala-Rincón. H-calculus: session types for hardware analysis and well-definedness. 2021. Dissertação (Mestrado em Informática) - Universidade de Brasília.
NANTES-SOBRINHO, DANIELE; Gomes da Silva, Samuel;Ayala-Rincon, M.. Técnicas Nominais e Aplicações em Lógica de Primeira Ordem. 2021. Dissertação (Mestrado em Matemática) - Universidade de Brasília.
Sobrinho, Daniele NantesVENTURA, Daniel Lima; Alves, Sandra;Ayala-Rincon, M.. A Study on May Solvability in the Resource Calculus. 2020. Dissertação (Mestrado em Matemática) - Universidade de Brasília.
NALON, Cláudia; Vieira, Bruno L.;Sobrinho, Daniele NantesM. Ayala-Rincón. A Resolution-Based E-connected Calculus. 2019. Dissertação (Mestrado em Informática) - Universidade de Brasília.
NANTES-SOBRINHO, DANIELE; Martins Ferreira, Francicleber;M. Ayala-Rincón. On Solving Nominal Disunification Constraints. 2019. Dissertação (Mestrado em Matemática) - Universidade de Brasília.
LLANOS, C. H.; da Silva, J. Y. M. A.;M. Ayala-Rincón. Employment of Parameter Adaptive Techniques to Bio-Inspired Meta-Heuristics for Mapping Real-Time Applications onto NoC based MPSoCs. 2019. Dissertação (Mestrado em Sistemas Mecatrônicos) - Universidade de Brasília.
LLANOS, C. H.; Fabro, A.T.;M. Ayala-Rincón. Surrogate-Assisted Optimization using Multi-Objective Evolutionary Techniques applied to Mechanical Structural Design. 2019. Dissertação (Mestrado em Sistemas Mecatrônicos) - Universidade de Brasília.
NANTES-SOBRINHO, DANIELE; HAEUSLER, Edward Hermann;Ayala-Rincón, Mauricio. Unificação Assimétrica Módulo Operadores Nilpotentes com Homomorfismo. 2017. Dissertação (Mestrado em Matemática) - Universidade de Brasília.
Weigang, Li; Ladeira, Marcelo; Cozman, Fabio Gagliardi; Carvalho, Rommel Novaes;M. Ayala-Rincón. PR-OWL 2 RL: um formalismo para tratamento de incerteza na Web semântica. 2016. Dissertação (Mestrado em Informática) - Universidade de Brasília.
ALVES, V. R.;Ayala-Rincón, Mauricio; TEIXEIRA, L. M.; MOTA, A. C.. Commuting Strategies for Product-Line Reliability Analysis. 2016. Dissertação (Mestrado em Informática) - Universidade de Brasília.
Weigang, Li; de Almeida Jr., Jorge Rady;Ayala-Rincón, Mauricio. Ligação de Entidades: uma nova abordagem para ligação de Conceitos Concretos com entidades Wiki utilizando MEV. 2015. Dissertação (Mestrado em Informática) - Universidade de Brasília.
Aranha, Diego de Freitas; van de Graff, Jeroen;Ayala-Rincón, Mauricio. Cifração e Autenticação utilizando Funções Fisicamente não Clonáveis (PUFs). 2014. Dissertação (Mestrado em Informática) - Universidade de Brasília.
MOURA, Flávio Leonardo Cavalcanti deVENTURA, Daniel LimaAyala-Rincon, M.. Um Estudo sobre Verificação Formal de Sistemas Concorrentes. 2012. Dissertação (Mestrado em Informática) - Universidade de Brasília.
ALVES, V. R.;Ayala-Rincón, Mauricio; ALVES, C. F.; GHEYI, R.. Especificação e verificação formais de boa-formação em linha de produtos de processo de negócios. 2012. Dissertação (Mestrado em Informática) - Universidade de Brasília.
PIMENTEL, E.; VERGARA, C. R. G.; RODRIGUES FILHO, A. A.;Ayala-Rincón, Mauricio. Sobre as lógicas linear, intuicionista e clássica e suas especificações. 2011. Dissertação (Mestrado em Matemática) - Universidade Federal de Minas Gerais.
MOURA, Flávio Leonardo Cavalcanti de; BENEVIDES, M.;Ayala-Rincón, Mauricio. Verificação de Propriedades do Cálculo Lambda ex em Coq. 2010. Dissertação (Mestrado em Informática) - Universidade de Brasília.
MOURA, Flávio Leonardo Cavalcanti deAyala-Rincón, Mauricio; RODRIGUES, P. H. A.. Uma Formalização de Propriedades de Composionalidade do cálculo Lambda ex em Coq. 2010. Dissertação (Mestrado em Informática) - Universidade de Brasília.
M. Ayala-RincónLLANOS, Carlos; VIDAL FILHO, Walter de Brito. SimRP - Simulador de Redes de Petri Flexível com Geração de Código VHDL. 2006. Dissertação (Mestrado em Engenharia Mecatrônica) - Universidade de Brasília.
M. Ayala-Rincón; MEIDANIS, João;WALTER, Maria Emilia Machado Telles. Ordenação por Transposição baseado no Formalismo Algébrico. 2006. Dissertação (Mestrado em Mestrado Em Informática) - Universidade de Brasília.
M. Ayala-Rincón; SAMPAIO, Marcus Costa; SAUVÉ, Jacques Philippe. Análise, Projeto e Implementação de um Esquema MOLAP de Data Warehouse, Utilizando o SGBD-OR Oracle 8.1. 2002. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal da Paraíba.
M. Ayala-Rincón; MATTOS, Luiz Antonio da Frota; FERNANDES, Clovis Torres. Infraestrutura Formal de Segurança para Sistemas Distribuídos. 2001. Dissertação (Mestrado em Ciência da Computação) - Universidade de Brasília.
M. Ayala-Rincón; JARDIM, Maria Helena Cautiero Horta; MAKLER, Susana Schleimberg de. Uma Extensão do Algoritmo Proximal para Programação Linear Quadrática Estendida. 1996. Dissertação (Mestrado em Matemática) - Universidade de Brasília.
HAEUSLER, Edward Hermann; Garcia, A. de V.; Rademaker, Alexandre; de Barros Santos, Jefferson;M. Ayala-Rincón. A proof in Lean about the Horizontal Compression of Dag-Like Derivations in Purely Implicational Minimal Logic. 2024. Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro.
WALTER, Maria Emilia Machado Telles; Dias, Zanoni; Kowada, L. A.;Ayala-Rincon, M.. Um novo algoritmo 1.375-aproximativo baseado em grupos de permutações para o Problema da Ordenação por Transposições. 2022. Tese (Doutorado em Informática) - Universidade de Brasília.
Thiemann, René;Ayala-Rincon, M.. Certifying Termination Proofs of LLVM IR Programs. 2022 - Universitat Innsbruck, Áustria.
HAEUSLER, Edward Hermann; Dowek, G.;Ayala-Rincón, Mauricio; BENEVIDES, M.; Vieira, Bruno L.; PEREIRA, Luiz Carlos P D; Laber, Eduardo Sany. Systems for Provability and Countermodel Generation in Propositional Minimal Implicational Logic. 2017. Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro.
TELLES, G. P.; GOG, S.; Laber, Eduardo Sany;M. Ayala-Rincón; Sadike Adi, S.; PEDROSA, L. L. C.. Engineering Augmented Suffix Sorting Algorithms. 2017. Tese (Doutorado em Ciência da Computação) - Universidade Estadual de Campinas.
QUEIROZ, R. G.; HAEUSLER, Edward Herman;MOURA, Flávio Leonardo Cavalcanti de; Bacelar, José Carlos; FREITAS, F. L. G.;Ayala-Rincón, Mauricio. Formalization of Context-Free Language Theory. 2016. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.
PIMENTEL, E.; Rueda, Camilo; Ortiz Rico, Guillermo;Ayala-Rincón, Mauricio. Sobre Extensiones Semánticas y Generalizaciones de Tipos en Lógica Lineal con Subexponenciales. 2016. Tese (Doutorado em Matemáticas) - Universidad Del Valle.
Nascimento, A.; Renner, Renato; Broadbent, Anne; Roetteler, Martin;Ayala-Rincón, Mauricio. Classical leakage-resilent circuits from quantum fault-tolerant computation. 2015. Tese (Doutorado em Informática) - Universidade de Brasília.
WELLS, J. B.; KAMAREDDINE, Fairouz;Ayala-Rincón, Mauricio; MICHAELSON, G.. New Developments to Skalpel: A Type Error Slicing Method for Explaining Errors in Type and Effect Systems. 2014. Tese (Doutorado em School of Mathematics and Computer Science) - Heriot-Watt University.
BONELLI, E.; RÍOS, Alejandro; KESNER, Delia; Aguirre, Nazareno; Miquel, Alexandre;Ayala-Rincón, Mauricio. Reduction spaces in non-sequential and infinitary rewriting systems. 2014. Tese (Doutorado em L'UFR d'informatique - Lab. PPS) - Université Paris Diderot.
HAEUSLER, Edward Hermann; Gordeev, Lew; Grisi de Oliveira, Anjolina;Ayala-Rincón, Mauricio; PEREIRA, Luiz Carlos P D; Casanova, Marco Antonio; BENEVIDES, M.. Some Results in a Proof-theory Based on Graphs. 2014. Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro.
Bonelli, Eduardo; CONIGLIO, Marcelo Esteban; Areces, Carlos;Ayala-Rincón, Mauricio. Dos temas en reescritura: combinadores para cálculos con patrones e isomorfismo de Curry-Howard para la Lógica de Pruebas. 2014. Tese (Doutorado em Ciencias de La Computación) - Universidad de Buenos Aires.
LLANOS, C. H.;Ayala-Rincón, Mauricio; HUEBNER, M.; CARVALHO, G. C.; BRAGA, A. P.. Redes Neurais Baseadas no Método de Grupo de Manipulação de Dados: treinamento, implementações e aplicações. 2013. Tese (Doutorado em Sistemas Mecatrônicos) - Universidade de Brasília.
QUEIROZ, R. G.; Scanlon, T.; Miraglia, F.; CONIGLIO, Marcelo Esteban;Ayala-Rincón, Mauricio. A Class of QFA Rings. 2011. Tese (Doutorado em Matemática) - Universidade Federal de Pernambuco.
BECKER, Jürgen; HARTENSTEIN, Reiner W;Ayala-Rincón, Mauricio; Jondral, Friedrich; Siegel, Michael; Neumann, Cornelius. A Flexible Framework for Hardware/Software Design Space Exploration using Rewriting Logic. 2010. Tese (Doutorado em Elektrotechnik und Informationstechnik) - Karlsruher Institut für Technologie.
HAEUSLER, Edward Hermann;M. Ayala-Rincón; Marcelo da Silva Corrêa; PEREIRA, Luiz Carlos P D; Geiza Maria Hamazaki Silva. Compactação de Provas Lógicas. 2007. Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro.
RÍOS, Alejandro;M. Ayala-Rincón; KESNER, Delia; SZASZ, Nora. Explicit Substitution: Systems and Subsystems. 2006. Tese (Doutorado em Ciencias de La Computación) - Universidad de Buenos Aires.
HAEUSLER, Edward Herman;M. Ayala-Rincón; VELOSO, Paulo A S; PEREIRA, Luiz Carlos P D; CONIGLIO, Marcelo Esteban. Extração de programas de provas. 2004. Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro.
de Araújo Bastos, R.;MOURA, Flávio Leonardo Cavalcanti de; ROCCO, Noraí Romeu;M. Ayala-Rincón. Teoria de Reescrita, Princípio de Resolução, Lógica Formal Computacional. 2024. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
dos Santos Lima, Igor; ROCCO, Noraí Romeu;MOURA, Flávio Leonardo Cavalcanti deAyala-Rincón, Mauricio. Teoria de Reescrita, Princípio de Resolução, Lógica Formal Computacional. 2024. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
Carrazedo Dantas, A.;Sobrinho, Daniele Nantes; ROCCO, Noraí Romeu;Ayala-Rincón, Mauricio. Teoria de Reescrita, Princípio de Resolução, Lógica Formal Computacional. 2024. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
KRASSALNIKOV, Alexei;Sobrinho, Daniele Nantes; ROCCO, Noraí Romeu;Ayala-Rincón, Mauricio. Teoria de Reescrita, Princípio de Resolução, Lógica Formal Computacional. 2024. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
Carrazedo Dantas, A.;Ayala-Rincón, MauricioSobrinho, Daniele Nantes; ROCCO, N. R.. Lógica Formal, Teoria de Reescrita e Princípio de Resolução. 2024. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
SHUMYATSKY, Pavel;Sobrinho, Daniele NantesAyala-Rincón, Mauricio; ROCCO, Noraí Romeu. Complexidade Computacional e Computabilidade, Resolução e Teoria de Reescrita. 2024. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
NANTES-SOBRINHO, DANIELE; FERNANDEZ, M.;VENTURA, Daniel LimaAyala-Rincón, Mauricio. Nominal C-Narrowing. 2024. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
To Fu Ma;De Lima, T.A.Sobrinho, Daniele NantesAyala-Rincón, Mauricio. Complexidade Computacional, Computabilidade, Resolução e Teoria de Reescrita. 2024. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
SHUMYATSKY, Pavel; ROCCO, Noraí Romeu; NANTES-SOBRINHO, DANIELE;Ayala-Rincón, Mauricio. Complexidade Computacional, Computabilidade, Resolução e Teoria de Reescrita. 2024. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
Ruviaro, Ricardo; ROCCO, Noraí Romeu; NANTES-SOBRINHO, DANIELE;Ayala-Rincón, Mauricio. Complexidade Computacional, Computabilidade, Resolução e Teoria de Reescrita. 2024. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
Carrazedo Dantas, A.;Ayala-Rincon, M.Sobrinho, Daniele Nantes; de Moura, Flávio L. C.. Teoria de Reescrita, Princípio de Resolução, Lógica Formal Computacional. 2024. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
de Araújo Bastos, R.; NANTES-SOBRINHO, DANIELE;De Lima, T.A.VENTURA, Daniel LimaM. Ayala-Rincón. Teoria de Tipos, Resolução e Reescrita - Segunda área teoria da computação. 2023. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
ROCCO, N. R.;De Lima, T.A.; de Moura, Flávio L. C.;M. Ayala-Rincón. Teoria de reescrita, princípio de resolução, lógica - Segunda área Teoria de Computação. 2023. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
Sobrinho, Daniele Nantes; Kutsia, T.; FERNANDEZ, M.;M. Ayala-Rincón. Nominal C-Disunification via Fixed-Point Constraints. 2023. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
dos Santos Lima, Igor;M. Ayala-RincónDe Lima, T.A.Sobrinho, Daniele Nantes. Teoria de Reescrita, Princípio de Resolução, Lógica Formal Computacional. 2023. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
ZALESSKI, Pavel;M. Ayala-RincónVENTURA, Daniel LimaSobrinho, Daniele Nantes. Teoria de Reescrita, Princípio de Resolução, Lógica Formal Computacional. 2023. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
PETROGRADSKIY, V.;M. Ayala-RincónMOURA, Flávio Leonardo Cavalcanti deDe Lima, T.A.. Teoria de Reescrita, Princípio de Resolução, Lógica Formal Computacional. 2023. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
GARONZI, M.;M. Ayala-RincónSobrinho, Daniele Nantes; de Moura, Flávio L. C.. Resolução, Lógica e Teoria de Prova. 2022. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
Carrazedo Dantas, A.; de Moura, Flávio L. C.;Sobrinho, Daniele NantesM. Ayala-Rincón. Qualificação Lógica Formal e Teoria de Reescrita. 2022. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
de Araújo Bastos, R.; HAEUSLER, Edward Herman; de Moura, Flávio L. C.;Sobrinho, Daniele NantesM. Ayala-Rincón. Qualificação Lógica Formal e Teoria de Reescrita. 2022. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
MELO, E. F.;Sobrinho, Daniele NantesDe Lima, T.A.Ayala-Rincon, M.. Teoria de reescrita e princípio de resolução. 2022. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
Kutsia, T.; Cerna, David;Sobrinho, Daniele NantesM. Ayala-Rincón. Anti-unificação módulo teoria de absorção. 2022. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
HAEUSLER, Edward Hermann; PEREIRA, Luiz Carlos P D; de Moura, Leonardo; de Barros Santos, Jefferson;M. Ayala-Rincón. A proof in Lean about the Horizontal Compression of Dag-Like Derivations in Implicational Logic. 2022. Exame de qualificação (Doutorando em Informática) - Pontifícia Universidade Católica do Rio de Janeiro.
Ayala-Rincon, M.; Navarro, Gonzalo; TELLES, G. P.;MELO, Alba Cristina Magalhaes Alves de; Claude-Faust, F. J.. Grammar Compression by Induced Suffix Sorting. 2021. Exame de qualificação (Doutorando em Informática) - Universidade de Brasília.
Sobrinho, Daniele NantesMOURA, Flávio Leonardo Cavalcanti deM. Ayala-Rincón. Teoria de Tipos, Reescrita e problemas equacionais. 2021. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
Sobrinho, Daniele NantesVENTURA, Daniel LimaAyala-Rincon, M.. Lógica Matemática e Teoria de Tipos -. 2020. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
HAEUSLER, Edward Herman;Sobrinho, Daniele NantesMOURA, Flávio Leonardo Cavalcanti deAyala-Rincon, M.. Unificação Nominal Módulo Teorias Equacionais. 2020. Exame de qualificação (Doutorando em Informática) - Universidade de Brasília.
HAEUSLER, Edward Herman;MOURA, Flávio Leonardo Cavalcanti deSobrinho, Daniele NantesM. Ayala-Rincón. Sistemas de Reescrita de Termos, Logica e Teoria de Prova. 2020. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
Rodrigues, G.N.;VENTURA, Daniel LimaAyala-Rincon, M.. O LambdaSigma Cálculo com todos os Índices de de Bruijn. 2020. Exame de qualificação (Doutorando em Informática) - Universidade de Brasília.
M. Ayala-Rincón; Moscato, Mariano; HAEUSLER, Edward Hermann; ALVES, V. R.; Muñoz, César. On Termination by Dependency Pairs andTermination of First-Order Functional Specificationsin PVS. 2020. Exame de qualificação (Doutorando em Informática) - Universidade de Brasília.
M. Ayala-Rincón; NANTES-SOBRINHO, DANIELE;MOURA, Flávio Leonardo Cavalcanti de. Topological Graphs, Lambda Calculus and Combinators. 2019. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
VENTURA, Daniel LimaMOURA, Flávio Leonardo Cavalcanti de; NALON, Cláudia;Ayala-Rincón, Mauricio. O LambdaSigma Cálculo com todos os Índices de de Bruijn. 2019. Exame de qualificação (Doutorando em Informática) - Universidade de Brasília.
MUNOZ, D.; Teodoro, George;M. Ayala-Rincón. Algoritmos Bioinspirados Multi-ilhas para Problemas de Alta Complexidade. 2018. Exame de qualificação (Doutorando em Informática) - Universidade de Brasília.
ROCCO, Noraí Romeu;VENTURA, Daniel LimaSobrinho, Daniele NantesM. Ayala-Rincón. Teoria da Computação - Teoria de Prova, Lógica Matemática e Computacional, Resolução e Teoria de Reescrita. 2018. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
SHUMYATSKY, Pavel;VENTURA, Daniel LimaMOURA, Flávio Leonardo Cavalcanti deM. Ayala-Rincón. Teoria da Computação - Teoria de Prova, Lógica Matemática e Computacional, Resolução e Teoria de Reescrita. 2018. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
SHUMYATSKY, Pavel; HAEUSLER, Edward Hermann;MOURA, Flávio Leonardo Cavalcanti deM. Ayala-Rincón. Teoria da Computação - Teoria de Prova, Lógica Matemática e Computacional, Resolução e Teoria de Reescrita. 2017. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
GARONZI, M.; HAEUSLER, Edward Hermann; NANTES-SOBRINHO, DANIELE;M. Ayala-Rincón. Teoria da Computação - Teoria de Prova, Lógica Matemática e Computacional, Resolução e Teoria de Reescrita. 2017. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
Sviridova, I.; HAEUSLER, Edward Hermann;MOURA, Flávio Leonardo Cavalcanti deM. Ayala-Rincón. Teoria da Computação - Teoria de Prova, Lógica Matemática e Computacional, Resolução e Teoria de Reescrita. 2017. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
TELLES, G. P.;WALTER, Maria Emilia Machado Telles; Teodoro, George;M. Ayala-Rincón. Dinamização de Estruturas de Dados Sucintas. 2016. Exame de qualificação (Doutorando em Informática) - Universidade de Brasília.
M. Ayala-Rincón; HAEUSLER, Edward Hermann; ALVES, V. R.;MOURA, Flávio Leonardo Cavalcanti de. Alpha-Equivalência, Matching e Unificação-Módulo na Sintaxe Nominal. 2016. Exame de qualificação (Doutorando em Informática) - Universidade de Brasília.
SHUMYATSKY, Pavel;Ayala-Rincón, Mauricio; HAEUSLER, Edward Herman;MOURA, Flávio Leonardo Cavalcanti de. Teoria da Computação - Lógica Matemática e Computacional, Resolução e Teoria de Reescrita. 2016. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
HAEUSLER, Edward Herman; ALVES, V. R.;MOURA, Flávio Leonardo Cavalcanti deM. Ayala-Rincón. Formalização da Equivalência entre Critérios de Terminação. 2016. Exame de qualificação (Doutorando em Informática) - Universidade de Brasília.
SHUMYATSKY, Pavel; HAEUSLER, Edward Hermann;MOURA, Flávio Leonardo Cavalcanti deM. Ayala-Rincón. Teoria da Computação - Lógica Matemática e Computacional, Resolução e Teoria de Reescrita. 2016. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
ROCCO, Noraí Romeu; BENEVIDES, M.;MOURA, Flávio Leonardo Cavalcanti deAyala-Rincón, Mauricio. Lógica Matemática e Computacional, Resolução e Teoria de Reescrita. 2015. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
TELLES, G. P.; Drummond, André; Brígido, Marcelo;M. Ayala-Rincón; Teodoro, George. Construção de Árvores Filogenéticas e o Problema da Mediana de Três Genomas. 2015. Exame de qualificação (Doutorando em Informática) - Universidade de Brasília.
QUEIROZ, R. G.;Ayala-Rincón, MauricioMOURA, Flávio Leonardo Cavalcanti de; FREITAS, F. L. G.. Language and Automata Theory Formalization. 2014. Exame de qualificação (Doutorando em Ciências da Computação) - Universidade Federal de Pernambuco.
HAEUSLER, Edward Herman; ALVES, V. R.;MOURA, Flávio Leonardo Cavalcanti deAyala-Rincón, Mauricio. Formalização de Reescrita Nominal em PVS. 2014. Exame de qualificação (Doutorando em Informática) - Universidade de Brasília.
SHUMYATSKY, Pavel; HAEUSLER, Edward Herman;MOURA, Flávio Leonardo Cavalcanti deAyala-Rincón, Mauricio. Teoria da Computação: teoria de reescrita e lógica formal. 2014. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
ZALESSKI, Pavel; HAEUSLER, Edward Herman;MOURA, Flávio Leonardo Cavalcanti deAyala-Rincón, Mauricio. Teoria da Computação: teoria de reescrita e lógica formal. 2014. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
ROCCO, Noraí Romeu; BENEVIDES, M.;MOURA, Flávio Leonardo Cavalcanti deAyala-Rincón, Mauricio. Teoria da Computação: teoria de reescrita e lógica formal. 2014. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
Godinho, Hemar T.; BENEVIDES, M.;MOURA, Flávio Leonardo Cavalcanti deAyala-Rincón, Mauricio. Teoria da Computação: teoria de reescrita e lógica formal. 2014. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
KRASSALNIKOV, Alexei; HAEUSLER, Edward Hermann;MOURA, Flávio Leonardo Cavalcanti deAyala-Rincón, Mauricio; PETROGRADSKIY, V.; BRANDAO JUNIOR, A. P.. Qualificação em Teoria da Computação e Álgebra. 2013. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
LLANOS, C. H.;JACOBI, Ricardo PAyala-Rincón, Mauricio; Coelho Abade, Gustavo. Solução Numérica de Sistemas Lineares Mediante o Uso de Arquiteturas Reconfiguráveis para Aplicações de Pequeno e Grande Porte. 2013. Exame de qualificação (Doutorando em Sistemas Mecatrônicos) - Universidade de Brasília.
Ayala-Rincón, Mauricio; HAEUSLER, Edward Hermann;MOURA, Flávio Leonardo Cavalcanti de; SHUMYATSKY, Pavel; ZALESSKI, Pavel; PINTO, A. G. S.. Qualificação em Teoria da Computação e Álgebra. 2011. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
Ayala-Rincón, MauricioNascimento, A.; HAEUSLER, Edward Hermann; PINTO, A. G. S.; SHUMYATSKY, Pavel; ZALESSKI, Pavel. Qualificação em Teoria da Computação e Álgebra. 2011. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
Ayala-Rincon, M.; FINGER, Marcelo;Nascimento, A.; ZALESSKI, Pavel; KRASSALNIKOV, Alexei; PINTO, A. G. S.. Teoria de Reescrita, Teoria de Prova e Criptografia. 2010. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
KRASSALNIKOV, Alexei;Ayala-Rincón, Mauricio; SHUMYATSKY, Pavel; HAEUSLER, Edward Hermann;MOURA, Flávio Leonardo Cavalcanti de; VIEIRA, A. C.. Qualificação em Álgebra e Teoria da Computação. 2009. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
HAEUSLER, Edward Hermann;MOURA, Flávio Leonardo Cavalcanti deM. Ayala-Rincón; ZALESSKI, Pavel; SHUMYATSKY, Pavel; SIDKI, Said. Qualificação em Álgebra e Teoria da Computação. 2008. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
HAEUSLER, Edward Hermann;MOURA, Flávio Leonardo Cavalcanti deM. Ayala-Rincón; SHUMYATSKY, Pavel; SIDKI, Said; ZALESSKI, Pavel. Qualificação em Álgebra e Teoria da Computação. 2008. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
SHUMYATSKY, Pavel; ZALESSKI, Pavel; FUTORNY, V.;MOURA, Flávio Leonardo Cavalcanti deAYALARINCON, M; HAEUSLER, Edward Hermann. Qualificação em Álgebra e Teoria da Computação. 2008. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
M. Ayala-Rincón; KRASSALNIKOV, Alexei; SHUMYATSKY, Pavel; NALON, Cláudia; HAEUSLER, Edward Herman; ZALESSKI, Pavel. Sistemas de tipos elaborados em cálculos de substituições explícitas. 2006. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
M. Ayala-Rincón; HAEUSLER, Edward Hermann; FINGER, Marcelo; SHUMYATSKY, Pavel; MAIER, Rudolf R; KRASSALNIKOV, Alexei. Implementação de estratêgias de demonstração da teoria de reescrita em assistentes de prova. 2005. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
M. Ayala-Rincón; HAEUSLER, Edward Hermann;POUBEL, Haydée Werneck; MAIER, Rudolf R; ROCCO, Noraí Romeu; SHUMYATSKY, Pavel. Unificação de ordem superior via cálculos de substituições explícitas para o caso dos patterns. 2003. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.
Martins, A.T.C.; FINGER, Marcelo; BENEVIDES, M.;Ayala-Rincon, M.. Presidente Comissão Avaliação Professora Claudia Nalon - Departamento de Computação Universidade de Brasília. 2022. Universidade de Brasília.
Ayala-Rincon, M.. King Saud University (KSU). 2022. King Saud University.
Ayala-Rincon, M.. Membro referees Academic and Research Staff Promotion - University of Kent (UK). 2021. University of Kent.
Ayala-Rincon, M.. Member Commission of External Evaluation. UTFSM (Chile). 2020. Universidad Tecnica Federico Santa Maria - Chile.
BENEVIDES, M.; Pereira, André G. C.;Ayala-Rincón, Mauricio; Bigonha, Roberto da Silva. Memorial - Prof. Elaine Gouvêa Pimentel - Departamento Matemática UFRN. 2018. Universidade Federal do Rio Grande do Norte.
WALTER, Maria Emilia Machado TellesAyala-Rincon, M.; TELLES, G. P.. Concurso para Professor Adjunto em Teoria de Computação. 2012. Universidade de Brasília.
Soares, Alexsandro S.; MATSUSHIGUE, C. A.;M. Ayala-Rincón. Concurso para Professor Adjunto na área de Teoria da Computação. 2008. Universidade Federal de Goiás.
M. Ayala-Rincón; HAEUSLER, Edward Hermann;WALTER, Maria Emilia Machado Telles; LUCERO, Jorge Carlos;POUBEL, Haydée Werneck. Concurso para Professor Adjunto na área de Teoria da Computação. 2005. Universidade de Brasília.
Orientou
Formalização e verificação de algoritmos de anti-unificação; Início: 2024; Dissertação (Mestrado profissional em Informática) - Universidade de Brasília; (Orientador);
Formalização algoritmos equacionais nominais; Início: 2024; Tese (Doutorado em Matemática) - Universidade de Brasília; (Orientador);
Anti-unificação para objetos de tipo arbitrário; Início: 2023; Tese (Doutorado em Matemática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; (Orientador);
Formalização de computações em ponto-flutuante em sistemas de gerenciamento de tráfego aéreo urbanos; Início: 2023; Tese (Doutorado em Informática) - Universidade de Brasília; (Orientador);
Raciocínio nominal equacional - anti-unificação (co-orientador Temur Kutsia RISC U; Linz); Início: 2021; Tese (Doutorado em Matemática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; (Orientador);
Improving the Safety of Numerical Programs; 2023; Dissertação (Mestrado em Informática) - Universidade de Brasília, ; Orientador: Mauricio Ayala Rincon;
A Study on Unification and Disunification Modulo; 2020; Dissertação (Mestrado em Informática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Mauricio Ayala Rincon;
Nominal Unification With Commutative and Associative-Commutative Function Symbols; 2019; Dissertação (Mestrado em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Formalização da Terminação de Especificações Funcionais; 2017; Dissertação (Mestrado em Informática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Distância de Translocação entre Genomas sem Sinal utilizando Algoritmos Genéticos; 2016; Dissertação (Mestrado em Informática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Mauricio Ayala Rincon;
Verificação de Implementações em Hardware por meio de Provas de Correção de suas Definições Recursivas; 2014; Dissertação (Mestrado em Informática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Mauricio Ayala Rincon;
Um índice baseado em árvores de sufixos comprimidas com baixo consumo de memória; 2013; Dissertação (Mestrado em Informática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Mauricio Ayala Rincon;
Ordenação por Reversões de Permutações sem Sinal Usando uma Abordagem de Algoritmos Genéticos; 2013; Dissertação (Mestrado em Informática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Mauricio Ayala Rincon;
Formalização da Confluência para Sistemas de Reescrita Ortogonais; 2012; Dissertação (Mestrado em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Expansibilidade em cálculos de substituições explícitas; 2012; Dissertação (Mestrado em Informática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Mauricio Ayala Rincon;
Ordenação de Sequências Finitas por Reversões Usando Conjugações em Grupos de Permutações; 2012; Dissertação (Mestrado em Informática) - Universidade de Brasília, ; Orientador: Mauricio Ayala Rincon;
Representação combinatória e algébrica das permutações na análise do problema de rearranjo de genomas por reversões; 2010; Dissertação (Mestrado em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Formalização da Prova do Teorema de Existência de Unificadores Mais Gerais em Teorias de Primeira-Ordem; 2009; Dissertação (Mestrado em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
O Problema da Dedução do Intruso para um Protocolo Criptográfico Especificado via Reescrita Módulo AC; 2009; Dissertação (Mestrado em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Verificação Formal de Protocolos Criptográficos - O Caso dos Protocolos em Cascata; 2008; 0 f; Dissertação (Mestrado em Mestrado Em Informática) - Universidade de Brasília, ; Orientador: Mauricio Ayala Rincon;
Cálculos de substituições explícitas que preservam a propriedade de redução de sujeito; 2006; 70 f; Dissertação (Mestrado em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Um algoritmo para pesquisa aproximada de padrões baseado no método de Landau Vishkin e uso de arranjos de sufixos para reduzir o uso de espaço; 2006; 80 f; Dissertação (Mestrado em Mestrado Em Informática) - Universidade de Brasília, ; Orientador: Mauricio Ayala Rincon;
SAEPTUM: Uma Metodologia de Verificação de Especificações de Sistemas de Reescrita por meio de Tradução a Teorias Lógicas; 2005; 0 f; Dissertação (Mestrado em Mestrado Em Informática) - Universidade de Brasília, ; Orientador: Mauricio Ayala Rincon;
Análise de Mecanismos para Combinar Passos de Beta-Contração em Cálculos de Substituições Explícitas; 2005; 70 f; Dissertação (Mestrado em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Deteção e Resolução Formal de Conflitos de Trafego Aéreo; 2004; 85 f; Dissertação (Mestrado em Matemática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Mauricio Ayala Rincon;
Comparação Entre Cálculos de Substituições Explícitas com Eta-Conversão; 2002; 70 f; Dissertação (Mestrado em Matemática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Mauricio Ayala Rincon;
Aplicação de Reescrita-Lógica na Especificação de Processadores; 2002; 70 f; Dissertação (Mestrado em Ciência da Computação) - Universidade de Brasília, ; Orientador: Mauricio Ayala Rincon;
Uma Modelagem Categórica para a Modularidade da Confluência em Sistemas de Reescrita de Termos; 2001; 100 f; Dissertação (Mestrado em Matemática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Coorientador: Mauricio Ayala Rincon;
Animação de Relações de Equivalência entre Modelos Computacionais, suas Gramáticas e Linguagens; 2001; 0 f; Dissertação (Mestrado em Ciência da Computação) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Mauricio Ayala Rincon;
Aplicacoes de Tecnicas de Reescrita ao Problema da Palavra em Teoria dos Grupos; 2000; Dissertação (Mestrado em Ciência da Computação) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Critérios de Confluência de Sistemas de Reescrita de Termos Lineares-Esquerdo Não Terminantes; 1998; 100 f; Dissertação (Mestrado em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Unificação Em Teorias Monoidais e Módulo A Aritmética de Presburger; 1998; 80 f; Dissertação (Mestrado em Matemática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Mauricio Ayala Rincon;
Formalismos dos Paradigmas de Programação Funcional e Lógica; 1997; 110 f; Dissertação (Mestrado em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Limite Inferior Para A Complexidade Dealgoritmos de Atualização de Árvores de Sufixos; 1997; 100 f; Dissertação (Mestrado em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Dynamically Reconfigurable Heterogeneous Parallel Island Model; 2024; Tese (Doutorado em Informática) - Universidade de Brasília, ; Orientador: Mauricio Ayala Rincon;
Towards Nominal AC-Unification; 2024; Tese (Doutorado em Informática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Mauricio Ayala Rincon;
Verifying the Computational Properties of a First-Order Functional Model; 2023; Tese (Doutorado em Informática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Mauricio Ayala Rincon;
Grammar Compression by Induced Suffix Sorting; 2022; Tese (Doutorado em Informática) - Universidade de Brasília, ; Orientador: Mauricio Ayala Rincon;
On Termination by Dependency Pairs and Termination of First-Order Functional Specifications in PVS; 2021; Tese (Doutorado em Informática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Mauricio Ayala Rincon;
Nominal Equational Problems Modulo Associativity, Commutativity and Associativity-Commutativity; 2019; Tese (Doutorado em Informática) - Universidade de Brasília, ; Orientador: Mauricio Ayala Rincon;
Cálculo da Distância de Reversão e Construção de Árvores Filogenéticas usando a Ordem dos Genes; 2017; Tese (Doutorado em Informática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Mauricio Ayala Rincon;
Unificação, Confluência e Tipos com Interseção para Sistemas de Reescrita Nominal; 2016; Tese (Doutorado em Informática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Mauricio Ayala Rincon;
Formalização da Automação da Terminação Através de Grafos com Matrizes de Medida; 2014; Tese (Doutorado em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Análise algébrico e combinatório do problema de rearranjo com técnicas de teoria de reescrita; 2014; Tese (Doutorado em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
O Problema da Dedução do Intruso para Teorias AC-convergentes Localmente Estáveis; 2013; Tese (Doutorado em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Cálculos de Substituições Explícitas à la de Bruijn com Sistemas de Tipos com Interseção; 2010; 0 f; Tese (Doutorado em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
A Flexible Framework for Hardware/Software Design Space Exploration using Rewriting Logic; 2010; Tese (Doutorado em Elektrotechnik und Informationstechnik) - Karlsruher Institut für Technologie, Deutscher Akademischer Austauschdienst; Coorientador: Mauricio Ayala Rincon;
Formalização da Teoria de Reescrita numa linguagem de ordem superior; 2008; 0 f; Tese (Doutorado em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Um estudo Comparativo em Unificação de Ordem Superior via Cálculos de Substituições Explícitas; 2006; 100 f; Tese (Doutorado em Matemática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Mauricio Ayala Rincon;
2015; Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Mauricio Ayala Rincon;
2014; Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Mauricio Ayala Rincon;
2013; Universidade de Brasília, ; Mauricio Ayala Rincon;
2011; Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Mauricio Ayala Rincon;
Formalização do Cálculo "Pointfree" em estilo relacional; 2014; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Universidade de Brasília; Orientador: Mauricio Ayala Rincon;
Correção e análise de algoritmos baseados no método Boyer-Moore de casamento de padrões; 2011; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Universidade de Brasília; Orientador: Mauricio Ayala Rincon;
Formalização em PVS de Teoremas Algébricos; 2025; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Formalização no assistente de prova PVS; 2024; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Formalização de viés em dados e algoritmos em PVS; 2023; Iniciação Científica; (Graduando em Estatística) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Construção de Protocolos Para Formalização de Viés em Dados e Procedimentos de Consulta e Recomendaçãa; 2022; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Formalização de propriedades algébricas para Quaternions em PVS; 2022; Iniciação Científica; (Graduando em Ciências da Computação) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Formalização de viés em dados e algoritmos em PVS; 2022; Iniciação Científica; (Graduando em Ciências da Computação) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Formalização da correção do algoritmo de Ford-Johnson; 2019; Iniciação Científica; (Graduando em Ciências da Computação) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Formalização de algoritmos de ordenação com ordens abstractos sobre um tipo não interpretado; 2018; Iniciação Científica; (Graduando em Engenharia Mecatrônica) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Formalização da Gödelização da Linguagem Funcional Minimal PVS0; 2017; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Fundação de Apoio à Pesquisa do Distrito Federal; Orientador: Mauricio Ayala Rincon;
Formalização de noções de complexidade computacional e de propriedades de algoritmos de ordenação; 2016; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Formalização de correcção de algoritmos em PVS; ; 2015; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Implementações de E-matching e E-unificação; 2015; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Formalização aplicada em problemas de otimização via polinômios de Bernstein; 2014; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Otimização por polinômios de Bernstein certificada; 2013; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Formalização de Protocolos de Selo Nominal; 2013; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Fundamentos de Formalização e Verificação; 2013; Iniciação Científica; (Graduando em Engenharia de Computação) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Mauricio Ayala Rincon;
Verificação formal em PVS de propriedades de segurança de sistemas criptográficos; 2012; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Formalização aplicada em problemas de otimização; 2012; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Formalização da segurança de protocolos em cascata com assinaturas; 2012; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade de Brasília; Orientador: Mauricio Ayala Rincon;
Modelagem e Formalização de Sistemas Computacionais utilizando Regras de Reescrita e Sistemas Dedutivos; 2011; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Verificação da Segurança de sistemas criptográficos; 2011; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Formalização de Propriedades de Segurança de Protocolos Criptográficos; 2010; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Teoria dos números e técnicas de fatoração eficientes; 2010; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Formaliização de Teoremas de Conflluência para Sistemas de Reescrita de Termos Lineares e Ortogonais; 2010; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Verificação e Formalização de sistemas criptográficos no assistente de demonstração PVS; 2010; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Formalização de Teoremas da Teoria dos Sistemas de Reescrita de Termos; 2009; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Verficação de Sistemas Reconfiguráveis: convoluções para processamento de imágens; 2009; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Aplicação de métodos formais na verificaçã de protocolos criptográficos; 2008; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Verificação de propriedades da teoria de reescrita utilizando o assistente de prova PVS; 2008; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Caracterização da propriedade de expansão em cálculos de substituições explícitas; 2008; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Estudo da Propriedade de Expansão para Cálculos de Substituições Explícitas; 2007; 0 f; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Demonstrações mecânicas baseadas em técnicas indutivas e da teoria de reescrita; 2007; 0 f; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Verificação formal de protocolos criptográficos; 2007; 0 f; Iniciação Científica; (Graduando em Engenharia de Redes) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Algoritmos exatos de seqüências biológicas em tempo sub-quadrático; 2006; 0 f; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Verificação de protocolos criptográficos utilizando PVS; 2006; 0 f; Iniciação Científica; (Graduando em Engenharia de Redes) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Implementação de Cálculos de Substituições Explícitas que Combinam Beta-Contração; 2005; 20 f; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Algoritmos Eficientes para Alinhamento de Seqüências; 2005; 0 f; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Verificação de Soluções Geométricas para Gerenciamento de Trafego Aéreo com PVS; 2005; 0 f; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Visualização da redução no cálculo lambda e em cáculos de substituições explícitas; 2004; 0 f; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Especificação de Sistemas de Reescrita para Simulação das Fases de Processadores Elaborados; 2003; 0 f; Iniciação Científica; (Graduando em Engenharia Mecatrônica) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Geração de Módulos de Sistemas Digitais Utilizando Técnicas de Reescrita; 2003; 0 f; Iniciação Científica; (Graduando em Engenharia Elétrica) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Visualização de Teoremas de Equivalência entre Modelos Computacionais e Representações Gramaticais: O caso das linguagens livres de contexto; 2002; 0 f; Iniciação Científica; (Graduando em Engenharia Mecatrônica) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Implementação da Unificação de Ordem Superior via o Lamda s_e-cálculo; 2002; 0 f; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Prova categórica da modularidade da terminalidade da união disjunta de sistemas de reescrita; 2002; 0 f; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Atualização Dinâmica de árvores de sufixos baseada em métodos de construção incremental; 2000; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Implementação de Algoritmos Gráficos para Ilustrar Relações de Equivalência de Modelos Computacionais; 2000; 30 f; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Implementacao de Algoritmos Graficos para Animar Algoritmos para Reconhecimento de Padroes em Palavras; 1999; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Formalização e Prova de Restrições de Integridade; 1997; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Demonstração automática de Teoremas Algébricos com Técnicas de Reescrita; 1997; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Formalização e Prova de Restrições de Integridade via Técnicas de Reescrita; 1997; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Implementação de algoritmos de decisão para a aritmética de Presburguer; 1996; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Estudo das propriedades dinâmicas das árvores de sufixos pra operações básicas e para geração de repetições em palavras; 1995; Iniciação Científica; (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Aplicações do Teorema de Church-Rosser (Bolsista PET Matemática UnB); 2015; Orientação de outra natureza; (Matemática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Mauricio Ayala Rincon;
Dedução natural no cálculo proposicional e de predicados para disciplina de Lógica Computacional; 2011; Orientação de outra natureza; (Ciência da Computação) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Mauricio Ayala Rincon;
Geração de material didático para lógica computacional; 2011; Orientação de outra natureza; (Ciência da Computação) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior; Orientador: Mauricio Ayala Rincon;
Aspetos implementacionais no sistema SUBSEXPL de cálculos de substituições explícitas que combinam Beta-contração: redução, normalizaçao, confluência, terminação (Bolsa DTI, projeto CT-INFO 506598/04-7 Modelagem Algorítmica, Semântica da Computação e Aplicações); 2006; 0 f; Orientação de outra natureza - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Mauricio Ayala Rincon;
Produções bibliográficas
-
da Silveira, Lucas A. ; DE LIMA, THAYNARA A. ; Ayala-Rincón, Mauricio . On reconfiguring heterogeneous parallel island models. Swarm and Evolutionary Computation , v. 89, p. 101624, 2024.
-
M. Ayala-Rincón ; FERNANDEZ, M. ; Ferreira Silva, G. ; Kutsia, T. ; NANTES-SOBRINHO, DANIELE . Certified First-Order AC-Unification and Applications. JOURNAL OF AUTOMATED REASONING , v. 68, p. 25-1-48, 2024.
-
SERRANO, F. ; De Lima, T.A. ; M. Ayala-Rincón . Compactness Theorem for Propositional Logic and Combinatorial Applications. Archive of Formal Proofs , v. 2024, p. 1-125, 2024.
-
Cesar Munoz ; M. Ayala-Rincón ; Moscato, Mariano ; Dutle, Aaron ; Narkawicz, Anthony ; Almeida, Ariane A. ; Avelar, Andréia B ; Ramos, T. M. F. . Formal Verification of Termination Criteria for First-Order Recursive Functions. JOURNAL OF AUTOMATED REASONING , v. 67, p. 1-30, 2023.
-
da Silveira, Lucas A. ; De Lima, T.A. ; LLANOS, C. H. ; M. Ayala-Rincón . On the behavior of parallel island models. APPLIED SOFT COMPUTING , v. 148, p. 110880, 2023.
-
NUNES, D. S. N. ; Louza, Felipe ; GOG, S. ; Ayala-Rincon, M. ; Navarro, Gonzalo . Grammar Compression by Induced Suffix Sorting. ACM JOURNAL OF EXPERIMENTAL ALGORITHMICS , v. 27, p. 1-33, 2022.
-
Ramos, Thiago M. Ferreira ; Almeida, Ariane A. ; Ayala-Rincón, Mauricio . Formalization of the Computational Theory of a Turing Complete Functional Language Model. JOURNAL OF AUTOMATED REASONING , v. 66, p. 1031-1063, 2022.
-
DE BARROS, JESSE BARRETO ; Anantharajaiah, N. ; Ayala-Rincón, Mauricio ; LLANOS, C. H. ; BECKER, Jürgen . The impact of formulation of cost function in Task Mapping Problem on NoCs using bio-inspired based-metaheuristics. MICROPROCESSORS AND MICROSYSTEMS , v. 94, p. 104668, 2022.
-
M. Ayala-Rincón ; de Carvalho-Segundo, Washington ; FERNANDEZ, M. ; Ferreira Silva, G. ; Sobrinho, Daniele Nantes . Formalising nominal C-unification generalised with protected variables. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE , v. 31, p. 286-311, 2021.
-
DE LIMA, THAYNARA ARIELLY ; GALDINO, André Luiz ; AVELAR, ANDRÉIA BORGES ; Ayala-Rincón, Mauricio . Formalization of Ring Theory in PVS. JOURNAL OF AUTOMATED REASONING , v. 65, p. 1231-1263, 2021.
-
M. Ayala-Rincón ; FERNANDEZ, M. ; NANTES-SOBRINHO, DANIELE ; Vale, Deivid . On Solving Nominal Disunification Constraints. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE , v. 348, p. 3-22, 2020.
-
M. Ayala-Rincón ; FERNANDEZ, M. ; NANTES-SOBRINHO, DANIELE . On Nominal Syntax and Permutation Fixed Points. Logical Methods in Computer Science , v. 16, p. 19:1-19:36, 2020.
-
ALMEIDA, A. A. ; Ayala-Rincón, Mauricio . Formalizing the dependency pair criterion for innermost termination. SCIENCE OF COMPUTER PROGRAMMING , v. 195, p. 102474, 2020.
-
Ayala-Rincón, Mauricio ; FERNÁNDEZ, MARIBEL ; NANTES-SOBRINHO, DANIELE ; ROCHA-OLIVEIRA, ANA CRISTINA . A formalisation of nominal α-equivalence with A, C, and AC function symbols. THEORETICAL COMPUTER SCIENCE , v. 781, p. 3-23, 2019.
-
Ayala-Rincón, Mauricio ; Bonelli, Eduardo ; Viso, Andres ; EDI, Juan . Typed Path Polymorphism. THEORETICAL COMPUTER SCIENCE , v. 781, p. 111-130, 2019.
-
SONCCO-ÁLVAREZ, JOSÉ LUIS ; MUÑOZ, DANIEL M. ; Ayala-Rincón, Mauricio . Opposition-Based Memetic Algorithm and Hybrid Approach for Sorting Permutations by Reversals. EVOLUTIONARY COMPUTATION (ONLINE) , v. 27, p. 229-265, 2019.
-
Ayala-Rincón, Mauricio ; de Carvalho-Segundo, Washington ; FERNÁNDEZ, MARIBEL ; NANTES-SOBRINHO, DANIELE . A Formalisation of Nominal C-Matching through Unification with Protected Variables. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE , v. 344, p. 47-65, 2019.
-
DE LIMA, THAYNARA ARIELLY ; Ayala-Rincón, Mauricio . On the average number of reversals needed to sort signed permutations. DISCRETE APPLIED MATHEMATICS , v. 235, p. 59-80, 2018.
-
M. Ayala-Rincón ; FERNANDEZ, M. ; Rocha Oliveira, Ana Cristina ; VENTURA, Daniel Lima . Nominal essential intersection types. THEORETICAL COMPUTER SCIENCE , p. 62-80, 2018.
-
ROCHA-OLIVEIRA, ANA CRISTINA ; GALDINO, André Luiz ; Ayala-Rincón, Mauricio . Confluence of Orthogonal Term Rewriting Systems in the Prototype Verification System. JOURNAL OF AUTOMATED REASONING , v. 58, p. 231-251, 2017.
-
Ayala-Rincón, Mauricio ; FERNÁNDEZ, MARIBEL ; NANTES-SOBRINHO, DANIELE . Intruder deduction problem for locally stable theories with normal forms and inverses. Theoretical Computer Science , v. 672, p. 64-100, 2017.
-
Ayala-Rincón, Mauricio ; FERNANDEZ, M. ; NANTES-SOBRINHO, DANIELE ; Carvalho Segundo, W.L.R. . A Formalisation of Nominal ? -equivalence with A and AC Function Symbols. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE , v. 332, p. 21-38, 2017.
-
Ayala-Rincón, Mauricio . Formalising Confluence in PVS. Electronic Proceedings in Theoretical Computer Science , v. 204, p. 11-17, 2016.
-
Ayala-Rincón, Mauricio ; FERNÁNDEZ, MARIBEL ; GABBAY, MURDOCH JAMES ; ROCHA-OLIVEIRA, ANA CRISTINA . Checking Overlaps of Nominal Rewriting Rules. Electronic Notes in Theoretical Computer Science , v. 323, p. 39-56, 2016.
-
Ayala-Rincón, Mauricio ; FERNÁNDEZ, MARIBEL ; ROCHA-OLIVEIRA, ANA CRISTINA . Completeness in PVS of a Nominal Unification Algorithm. Electronic Notes in Theoretical Computer Science , v. 323, p. 57-74, 2016.
-
VISO, ANDRÉS ; Bonelli, Eduardo ; Ayala-Rincón, Mauricio . Type Soundness for Path Polymorphism. Electronic Notes in Theoretical Computer Science , v. 323, p. 235-251, 2016.
-
NOGUEIRA NUNES, DANIEL SAAD ; Ayala-Rincón, Mauricio . A Practical Semi-External Memory Method for Approximate Pattern Matching. Electronic Notes in Theoretical Computer Science , v. 324, p. 107-122, 2016.
-
Soncco-Álvarez, J.L. ; ALMEIDA, G. M. ; BECKER, Jürgen ; Ayala-Rincón, Mauricio . Parallelization of genetic algorithms for sorting permutations by reversals over biological data. International Journal of Hybrid Intelligent Systems , v. 12, p. 53-64, 2015.
-
VENTURA, D. L. ; Kamareddine, F. ; Ayala-Rincon, M. . Explicit substitution calculi with de Bruijn indices and intersection type systems. Logic Journal of the IGPL (Print) , v. 23, p. 295-340, 2015.
-
NUNES, D. S. N. ; Ayala-Rincón, Mauricio . A Compressed Suffix Tree Based Implementation With Low Peak Memory Usage. Electronic Notes in Theoretical Computer Science , v. 302, p. 73-94, 2014.
-
Avelar, Andréia B ; GALDINO, André Luiz ; MOURA, Flávio Leonardo Cavalcanti de ; M. Ayala-Rincón . First-order unification in the PVS proof assistant. Logic Journal of the IGPL (Print) , p. 758-789, 2014.
-
MUÑOZ, DANIEL M. ; LLANOS, CARLOS H. ; COELHO, LEANDRO DOS S. ; Ayala-Rincón, Mauricio . Hardware opposition-based PSO applied to mobile robot controllers. Engineering Applications of Artificial Intelligence , v. 28, p. 64-77, 2014.
-
Soncco-Álvarez, J.L. ; Ayala-Rincon, M. . Sorting Permutations by Reversals through a Hybrid Genetic Algorithm based on Breakpoint Elimination and Exact Solutions for Signed Permutations. Electronic Notes in Theoretical Computer Science , v. 292, p. 119-133, 2013.
-
Ayala-Rincón, Mauricio ; FERNÁNDEZ, MARIBEL ; NANTES-SOBRINHO, DANIELE . Elementary Deduction Problem for Locally Stable Theories with Normal Forms. Electronic Proceedings in Theoretical Computer Science , v. 113, p. 45-60, 2013.
-
Santos Rego, Yuri ; M. Ayala-Rincón . Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model. JOURNAL OF FORMALIZED REASONING , v. 6, p. 31-61, 2013.
-
Rocha Oliveira, Ana Cristina ; Ayala-Rincón, Mauricio . Formalizing the Confluence of Orthogonal Rewriting Systems. Electronic Proceedings in Theoretical Computer Science , v. 113, p. 145-152, 2013.
-
Avelar, Andréia B ; GALDINO, ANDRÉ L ; DE MOURA, FLÁVIO LC ; Ayala-Rincón, Mauricio . A Formalization of the Theorem of Existence of First-Order Most General Unifiers. Electronic Proceedings in Theoretical Computer Science , v. 81, p. 63-78, 2012.
-
de Moura, F.L.C. ; Barbosa, Alex ; M. Ayala-Rincón . A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi. Electronic Notes in Theoretical Computer Science , v. 269, p. 41-54, 2011.
-
ARBOLEDA, Daniel Muñoz ; SANCHEZ, D. F. ; LLANOS, Carlos ; Ayala-Rincón, Mauricio . Tradeoff of FPGA Design of a Floating-point Library for Arithmetic Operators. JICS. JOURNAL OF INTEGRATED CIRCUITS AND SYSTEMS (ED. PORTUGUÊS) , v. 5, p. 42-52, 2010.
-
Galdino, André L. ; Ayala-Rincón, Mauricio . A Formalization of the Knuth-Bendix(-Huet) Critical Pair Theorem. Journal of Automated Reasoning , v. 45, p. 301-325, 2010.
-
Ventura, D. ; Ayala-Rincon, M. ; Kamareddine, F. . Explicit substitutions calculi with one step Eta-reduction decided explicitly. Logic Journal of the IGPL , v. 17, p. 697-718, 2009.
-
Galdino, André L. ; Ayala-Rincón, Mauricio . A PVS Theory for Term Rewriting Systems. Electronic Notes in Theoretical Computer Science , v. 247, p. 67-83, 2009.
-
MOURA, Flávio Leonardo Cavalcanti de ; M. Ayala-Rincón ; KAMAREDDINE, Fairouz . Higher-Order Unification: a structural relation between Huet's method and the one based on explicit substitutions (comunicado por Dov M. Gabbay). Journal of Applied Logic , Holanda, v. 6, p. 72-108, 2008.
-
ARBOLEDA, Daniel Muñoz ; LLANOS, Carlos ; M. Ayala-Rincón ; van ELS, R. . Distributed approach to group control of elevator systems using fuzzy logic and FPGA implementation of dispatching algorithms. Engineering Applications of Artificial Intelligence , v. 21, p. 1309-1320, 2008.
-
GALDINO, André Luiz ; AYALARINCON, M . A Formalization of Newman's and Yokouchi's Lemmas in a Higher-Order Language. JOURNAL OF FORMALIZED REASONING , v. 1, p. 39-50, 2008.
-
GALDINO, André Luiz ; AYALARINCON, M . A Theory for Abstract Reduction Systems in PVS. CLEI ELECTRONIC JOURNAL , v. 11, p. 1-12, 2008.
-
BOUKERCHE, Azzedine ; MELO, Alba Cristina Magalhaes Alves de ; SANDES, Edans Flávius de Oliveira ; M. Ayala-Rincón . An Exact Parallel Algorithm to Compare Very Long Biological Sequences in Clusters of Workstations. Cluster Computing , USA, v. 10, p. 187-202, 2007.
-
M. Ayala-Rincón ; ABREU, Bruno T de ; SIQUEIRA, José de . A Variant of the Ford-Johnson Algorithm that is more Space Efficient (comunicado por F. M. auf der Heide). Information Processing Letters , Holanda, v. 102, p. 201-207, 2007.
-
BOUKERCHE, Azzedine ; MELO, Alba Cristina Magalhaes Alves de ; M. Ayala-Rincón ; WALTER, Maria Emilia Machado Telles . Parallel Strategies for Local Biological Sequence Alignment. Journal of Parallel and Distributed Computing , Holanda, v. 67, n.2, p. 170-185, 2007.
-
M. Ayala-Rincón ; LLANOS, Carlos ; JACOBI, Ricardo P ; HARTENSTEIN, Reiner W . Prototyping Time and Space Effiicient Computations of Algebraic Operations over Dynamically Reconfigurable Systems Modeled by Rewriting-Logic. ACM Transactions on Design Automation of Electronic Systems , USA, v. 11, n.2, p. 251-281, 2006.
-
MOURA, Flávio Leonardo Cavalcanti de ; M. Ayala-Rincón ; KAMAREDDINE, Fairouz . SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi -. Journal of Applied Non-Classical Logics , Paris, v. 16, n.1-2, p. 119-150, 2006.
-
M. Ayala-Rincón ; MOURA, Flávio Leonardo Cavalcanti de ; KAMAREDDINE, Fairouz . Comparing and Implementing Calculi of Explicit Substitutions with Eta Reduction. Annals of Pure and Applied Logic , Amsterdam, v. 134, n.1, p. 5-41, 2005.
-
JACOBI, Ricardo P ; M. Ayala-Rincón ; CARVALHO, Luis G A ; LLANOS, Carlos ; HARTENSTEIN, Reiner W . Reconfigurable Systems for Sequence Alignment and for General Dynamic Programming. GENETICS AND MOLECULAR RESEARCH , Brasil, v. 4, n.3, p. 543-552, 2005.
-
KAMAREDDINE, Fairouz ; MONIN, François ; M. Ayala-Rincón . On Automating the Extraction of Programs from Termination Proofs. Revista Colombiana de Computación , v. 4, n.2, p. 29-48, 2004.
-
M. Ayala-Rincón ; CONEJO, P. D. . A Linear Time Lower Bound on McCreight and General Updating Algorithms for Suffix Trees. Algorithmica , New York, v. 37, n.3, p. 233-241, 2003.
-
M. Ayala-Rincón ; KAMAREDDINE, Fairouz . On applying the lambda s_e-style of unification for simple typed higher-order unification in the pure lambda-calculus. Matemática Contemporânea , v. 24, p. 1-22, 2003.
-
M. Ayala-Rincón ; HARTENSTEIN, Reiner W ; NETO, R. M. ; JACOBI, Ricardo P ; LLANOS, Carlos . Architectural Specification, Exploration and Simulation Through Rewriting-Logic. Revista Colombiana de Computación , Colômbia, v. 3, n.2, p. 20-34, 2003.
-
M. Ayala-Rincón ; FONSECA, A. F. ; POUBEL, Haydée Werneck ; SIQUEIRA, José de . A Framework to Visualize Equivalences Between Computational Models of Regular Languages. Information Processing Letters , v. 84, n.1, p. 5-16, 2002.
-
M. Ayala-Rincón ; ARAÚJO, I. E. T. . Unification Modulo Presburger Arithmetic and Other Decidable Theories. Revista Colombiana de Computación , v. 2, n.2, p. 7-19, 2002.
-
M. Ayala-Rincón ; MAYA NETO, R. ; LLANOS, C. H. ; HARSTEINER, R. ; JACOBI, R. P. . Applying ELAN Strategies in Simulating Processors over Simple Architectures. Electronic Notes in Theoretical Computer Science , v. 70, n.6, p. 84-99, 2002.
-
M. Ayala-Rincón ; FONSECA, A. F. ; SILVA, A. H. R. ; POUBEL, Haydée Werneck ; SIQUEIRA, José de . Animation of Relations Between Computational Models and Languages. Bulletin of the European Association for Theoretical Computer Science , v. 74, p. 235-241, 2001.
-
M. Ayala-Rincón ; KAMAREDDINE, Fairouz . Unification via the Lambda s_e Style of Explicit Substitutions. Logic Journal of the IGPL , Inglaterra, v. 9, n.4, p. 489-521, 2001.
-
M. Ayala-Rincón ; Cesar Munoz . Explicit Substitutions and All That. Revista Colombiana de Computación , v. 1, n.1, p. 47-71, 2000.
-
M. Ayala-Rincón . A Deductive Calculus For Conditional Equational Systems With Built-In Predicates As Premises. Revista Colombiana de Matemáticas , Colômbia, v. 31, n.2, p. 77-98, 1997.
-
M. Ayala-Rincón ; L. M. R. Gadelha . Some Applications Of (Semi-)Decision Algorithms For Presburger Arithmetic In Automated Deduction Based On Rewriting Techniques. Revista de la Sociedad Chilena de Ciencia de la Computación , Chile, v. 2, n.1, p. 14-23, 1997.
-
M. Ayala-Rincón . Problemas Actuales en el Campo de La Reescritura. Revista de la Escuela Colombiana de Ingenierías , Bogotá, Colômbia, v. 4, n.10, p. 27-31, 1993.
-
Ayala-Rincon, M. ; Bonelli, Eduardo (Org.) . Proceedings 16th Logical and Semantic Frameworks with Applications. 1. ed. Cornell University: EPTCS vol 357, 2022. v. 1. 130p .
-
M. Ayala-Rincón ; Mimram, S. (Org.) . Special Issue of Mathematical Structures in Computer Science, on confluence, vol 32(7). 1. ed. Cambridge: Cambridge University Press, 2022. v. 1. 200p .
-
M. Ayala-Rincón ; Balbiani, Philippe (Org.) . Special Issue of Mathematical Structures in Computer Sciences Vol 30 Issue 6, on Unification. 1. ed. Cambridge: Cambridge University Press, 2020. v. 1. 200p .
-
M. Ayala-Rincón ; Mimram, S. (Org.) . Proceedings 9th International Workshop on Confluence. 1. ed. Paris: Paris Nord Summer of LoVe 2020, LOgic and VErification at Université Paris 13, 2020. v. 1. 100p .
-
M. Ayala-Rincón ; Muñoz, César (Org.) . Special Issue of Journal of Automated Reasoning, Vol. 63(2), on Interactive Theorem Proving. 1. ed. Springer Nature, 2019. 300p .
-
M. Ayala-Rincón ; Ghilzean, S. (Org.) ; Grue Simonsen, J. (Org.) . Joint Proceedings of HOR 2019 and IWC 2019 (with system descriptions from CoCo 2019). 1. ed. Brasilia, Novi Sad, Copenhagen: FSCD 2019, 2019. v. 1. 100p .
-
M. Ayala-Rincón ; Balbiani, Philippe (Org.) . Pre-proceedings 32nd International Workshop on Unification UNIF 2018. 1. ed. Brasília/Toulouse: FSCD/FLOC 2018 (Oxford) Affiliated Workshop, 2018. v. 1. 100p .
-
Ayala-Rincon, M. ; MOURA, Flávio Leonardo Cavalcanti de . Applied Logic for Computer Scientists - Computational Deduction and Formal Proofs. 1. ed. Heidelberg: Springer International, 2017. 200p .
-
Ayala-Rincón, Mauricio ; MACKIE, I. (Org.) ; Montanari, Ugo (Org.) . Special Issue of Theoretical Computer Science, Vol. 685, Logical and Semantic Frameworks with Applications. 1. ed. Amsterdam: Elsevier, 2017. v. 1. 150p .
-
Ayala-Rincón, Mauricio ; Cesar Munoz (Org.) . Interactive Theorem Proving, 8th International Conference, ITP 2017, LNCS Proceedings. 1. ed. Heidelberg: Springer International Publishing, 2017. v. 10499. 514p .
-
Ayala-Rincón, Mauricio ; MACKIE, I. (Org.) . ELSEVIER ENTCS, Vol. 312, Proceedings 9th Logical and Semantic Frameworks with Applications LSFA 2014. 1. ed. Amsterdam: Elsevier ENTCS - Electronic Notes in Theoretical Computer Science, 2015. v. 312. 252p .
-
M. Ayala-Rincón ; Bonelli, Eduardo (Org.) ; MACKIE, I. (Org.) . Cornell U. EPTCS, Vol. 144, Proceedings 9th International Workshop on Developments in Computational Models. 1. ed. Cornell University Library, 2014. v. 144. 95p .
-
Ayala-Rincón, Mauricio ; MOURA, Flávio Leonardo Cavalcanti de . FUNDAMENTOS DA PROGRAMAÇÃO LÓGICA E FUNCIONAL: O PRINCÍPIO DE RESOLUÇÃO E A TEORIA DE REESCRITA. 1. ed. Brasilia: UnB, 2014. 250p .
-
Ayala-Rincon, M. ; PIMENTEL, E. (Org.) ; KAMAREDDINE, Fairouz (Org.) . Special Issue of Theoretical Computer Science, Volume 412(37), Logical and Semantic Frameworks with Applications - Guest Editor. Amsterdam: ELSEVIER, 2011. v. 412-37. 200p .
-
AYALARINCON, M ; HAEUSLER, Edward Hermann (Org.) . Special Issue of The Logical Journal of the IGPL, Vol. 17(5), Second Logical and Semantic Frameworks, with Applications - Guest Editor. 1. ed. Oxford: Oxford University Press, 2009. v. 17(5). 110p .
-
Ayala-Rincon, M. ; KAMAREDDINE, Fairouz (Org.) . ELSEVIER ENTCS, Vol. 256, Proceedings of the 4th Logical and Semantic Frameworks with Applications LSFA 2009. 1. ed. Amsterdam: Elsevier ENTCS - Electronic Notes in Theoretical Computer Science, 2009. v. 256. 140p .
-
M. Ayala-Rincón ; HAEUSLER, Edward Hermann (Org.) . ELSEVIER ENTCS, Vol. 205, Proceedings 2nd Workshop on Logical and Semantic Frameworks, with Applications. 1. ed. Amsterdam: Elsevier ENTCS - Electronic Notes in Theoretical Computer Science, 2008. v. 205. 129p .
-
M. Ayala-Rincón ; HAEUSLER, Edward Hermann (Org.) ; BRAGA, Christiano (Org.) . Pré-proceedings of the Brazilian Workshop on Logical and Semantic Frameworks, with Applications LSFA2006. Natal: SBC/UFRN, 2006. v. 1. 70p .
-
M. Ayala-Rincón ; QUEIROZ, R. G. (Org.) . Pre-Proc. Eighth Workshop on Logic, Language, Information and Computation. Brasília: CESPE/UnB, 2001. v. 1. 155p .
-
Ayala-Rincón, Mauricio ; DE LIMA, THAYNARA ARIELLY ; Lima, Maria Júlia Dias ; Moscato, Mariano Miguel ; Kutsia, Temur . Verification of an Anti-unification Algorithm in PVS. Lecture Notes in Computer Science. 1ed.: Springer Nature Switzerland, 2025, v. 15682, p. 54-71.
-
Ayala-Rincón, Mauricio ; Cerna, David M. ; Barragán, Andrés Felipe González ; Kutsia, Temur . Equational Anti-unification over Absorption Theories. In: Christoph Benzmüller; Marijn J.H. Heule; Renate A. Schmidt. (Org.). Lecture Notes in Computer Science. 1ed.: Springer Nature Switzerland, 2024, v. 14740, p. 317-337.
-
Ayala-Rincón, Mauricio ; FERNÁNDEZ, MARIBEL ; NANTES-SOBRINHO, DANIELE ; Vale, Deivid . Nominal Equational Problems. In: Foundations of Software Science and Computation Structures. FOSSACS 2021. (Org.). Lecture Notes in Computer Science. 1ed.: Springer International Publishing, 2021, v. 12650, p. 22-41.
-
Alvarez-Mamani, Edwin ; Enciso-Rodas, Lauro ; Ayala-Rincón, Mauricio ; Soncco-Álvarez, José L. . Parallel Social Spider Optimization Algorithms with Island Model for the Clustering Problem. Communications in Computer and Information Science. 1ed.: Springer International Publishing, 2021, v. , p. 122-138.
-
Almeida, Ariane A. ; ROCHA-OLIVEIRA, ANA CRISTINA ; Ramos, Thiago M. Ferreira ; de Moura, Flávio L. C. ; Ayala-Rincón, Mauricio . The Computational Relevance of Formal Logic Through Formal Proofs. Lecture Notes in Computer Science. 1ed.Springer LNCS, Heidelberg: Springer International Publishing, 2019, v. 11758, p. 81-96.
-
da Silveira, Lucas A. ; Soncco-Álvarez, José L. ; DE LIMA, THAYNARA A. ; Ayala-Rincón, Mauricio . Memetic and Opposition-Based Learning Genetic Algorithms for Sorting Unsigned Genomes by Translocations. Advances in Intelligent Systems and Computing. 1ed.Berling, Heidelberg: Springer International Publishing, 2016, v. 419, p. 73-85.
-
HAEUSLER, Edward Hermann ; Ayala-Rincón, Mauricio . On the Computability of Relations on λ-Terms and Rice’s Theorem - The Case of the Expansion Problem for Explicit Substitutions. Lecture Notes in Computer Science. 1ed.Heidelberg: Springer Berlin Heidelberg, 2014, v. 8392, p. 202-213.
-
VENTURA, Daniel Lima ; AYALARINCON, M ; KAMAREDDINE, Fairouz . Intersection Type System with de Bruijn Indices. In: M. Coniglio; W. Carnielli; I. D'Ottaviano. (Org.). The Many Sides of Logic,. London: College Publications, London, 2009, v. 21, p. 557-576.
-
M. Ayala-Rincón . Church-Rosser Property For Conditional Rewriting Systems With Built-In Predicates As Premises. In: M. del Rijke and D. V. Gabbay (Editors). (Org.). Frontiers of combinning systems 2 (Studies in Logic and Computation. Baldock, Inglaterra: Research Studies Press / John Wiley & Sons, 2000, v. 7, p. 17-38.
-
M. Ayala-Rincón ; FERNANDEZ, M. ; NANTES-SOBRINHO, DANIELE ; de Souza, D. S. M. . Nominal Equational Rewriting and Narrowing. In: 19th Logical and Semantic Frameworks with Applications - LSFA 2024, 2025, Goiânia. Póst-proceedings LSFA 2024 - Edited by Cynthia Kop and Helida Salles Santos. Edinburgh: EPTCS, 2025. v. 421. p. 80-97.
-
Ayala-Rincón, Mauricio ; Cerna, David M. ; Kutsia, T. ; Ringeissen, C. . Combining Generalization Algorithms in Regular Collapse-Free Theories. In: 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025), 2025, Birmingham. LIPIcs Proc. 10th 10th International Conference on Formal Structures for Computation and Deduction. Dagstuhl: Leibniz International Proceedings in Informatics (LIPIcs), 2025. v. 337. p. 7:1-7:18.
-
De Lima, T.A. ; GALDINO, André Luiz ; Resende, B. B. O. ; M. Ayala-Rincón . A Formalization of the General Theory of Quaternions. In: International Conference on Interactive Theorem Proving, 2024, Tblisi. LiPIcs Proc. 15th International Conference on Interactive Theorem Proving (ITP). Dagstuhl: LiPIcs, 2024. p. 27:1-27:18.
-
González Barragán, A. F. ; Cerna, David M. ; Ayala-Rincón, Mauricio ; Kutsia, Temur . On Anti-Unification over Absorption, Associative, and Commutative Theories. In: 38th International Workshop on Unification / UNIF 2024, Affiliated to IJCAR 2024, 2024, Nancy. Proceedings UNIF 2024 LTCS-Report 24-04 Technische Universität Dresden. Dresden: LTCS-Report 24-04 Technische Universität Dresden, 2024. v. 24. p. 56-61.
-
Ferreira, Gabriela de Souza ; Cerna, David M. ; Ayala-Rincón, Mauricio ; Kutsia, Temur . Computing Generalizers over Intersection and Union Type Theories. In: 38th International Workshop on Unification UNIF 2024 - Affiliated to IJCAR, 2024, Nancy. Proceedings 38th International Workshop on Unification UNIF 2024 - Affiliated to IJCAR. Dresden: LTCS-Report 24-04 Technische Universität Dresden, 2024. v. 24. p. 62-68.
-
Cerna, David ; González Barragán, A. F. ; M. Ayala-Rincón ; Kutsia, T. . Anti-unification on Absorption and Commutative Theories. In: 19th Logical and Semantic Frameworks with Applications - LSFA 2024, 2024, Goiânia. Pré-proceedings LSFA 2024 - Edited by Cynthia Kop. Goiânia: UFG, 2024. p. 105-121.
-
Ayala-Rincón, Mauricio ; ARIELLY DE LIMA, THAYNARA ; AVELAR, ANDRÉIA B. ; GALDINO, André Luiz . Formalization of Algebraic Theorems in PVS (Invited Talk). In: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2023, Manizales. org.crossref.xschema._1.Title@389b97c. Manchester: EasyChair - EPiC Series in Computing, 2023. v. 94. p. 1-10.
-
SERRANO, F. ; M. Ayala-Rincón ; De Lima, T.A. . Mechanising Hall's Theorem for Countable Graphs. In: 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning - LPAR, 2023, Manizales. EasyChair Preprint Presented at 24th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning - LPAR-24. Manchester: EasyChair Preprint, 2023. v. 10365. p. 1-14.
-
DE LIMA, THAYNARA A. ; Galdino, André L. ; AVELAR, ANDRÉIA BORGES ; M. Ayala-Rincón . Formalization of Factorization on Euclidean Domains and Euclidean Algorithms. In: 18th Logical and Semantic Frameworks with Applications LSFA, 2023, Roma. Proc. LSFA 2023. EasyChair: EPTCS, 2023. p. 1-17.
-
M. Ayala-Rincón . Formalisation of Nominal Equational Reasoning (Invited Talk). In: 37th International Workshop on Unification UNIF 2024, 2023, Roma. HAL Proceedings 37th International Workshop on Unification. Paris: HAL Open Science CNRS/INRIA, 2023. p. 1-7.
-
M. Ayala-Rincón ; FERNANDEZ, M. ; Ferreira Silva, G. ; Kutsia, T. ; NANTES-SOBRINHO, DANIELE . Nominal AC-matching. In: The 16th Conference on Intelligent Computer Mathematics - CICM 2023, 2023, Cambridge. LNCS (LNAI) Proc. The 16th Conference on Intelligent Computer Mathematics. Cham (Suiça): Springer Nature Switzerland, 2023. v. 14101. p. 53-68.
-
Fernandes Ferreira, N. B. ; Moscato, Mariano ; Titolo, L. ; M. Ayala-Rincón . A provably correct floating-point implementation of Well Clear Avionics Concepts. In: 23rd Int. Conf. on Formal Methods in Computer-Aided Design - FMCAD 2023, 2023, Ames. TU Wien AP Proc. 23rd Int. Conf. on Formal Methods in Computer-Aided Design - FMCAD 2023. Wien: TU Wien Academic Press / IEEE Explore, 2023. p. 237-246.
-
González Barragán, A. F. ; Cerna, David ; Kutsia, T. ; Ayala-Rincón, Mauricio . On Anti-unification in Absorption Theories. In: 37th International Workshop on Unification UNIF 2023, 2023, Roma. Proceedings 37th International Workshop on Unification. Paris: HAL Open Science CNRS/INRIA, 2023. p. 1-7.
-
M. Ayala-Rincón ; FERNANDEZ, M. ; Ferreira Silva, G. ; Sobrinho, Daniele Nantes . A Certified Algorithm for AC-Unification. In: 7th International Conference on Formal Structures for Computation and Deduction FSCD, 2022, Haifa. LiPIcs Proceedings FSCD 2022. Dagstuhl: LiPIcs, 2022. v. 1. p. 1-24.
-
SERRANO, F. ; De Lima, T.A. ; M. Ayala-Rincón . Hall?s Theorem for Enumerable Families of Finite Sets. In: 15th Int. Conference on Intelligent Computer Mathematics CICM 2022, 2022, Tiblist. Springer LNCS Proceedings 15th Int. Conference on Intelligent Computer Mathematics CICM 2022. Heidelberg: Springer Nature. v. 13467. p. 107-121.
-
da Silveira, Lucas A. ; DE LIMA, THAYNARA A. ; AYALA-RINCON, MAURICIO . Reconfigurable Heterogeneous Parallel Island Models. In: 2022 IEEE Symposium Series on Computational Intelligence (SSCI), 2022, Singapore. 2022 IEEE Symposium Series on Computational Intelligence (SSCI). New York: IEEE, 2022. p. 1618-8.
-
Muñoz, César ; M. Ayala-Rincón ; Moscato, Mariano ; Dutle, Aaron ; Narkawicz, Anthony ; ALMEIDA, A. A. ; Avelar, Andréia B ; Ramos, T. M. F. . Formal Verification of Termination Criteria for First-Order Recursive Functions. In: 12th International Conference on Interative Theorem Proving, 2021, Roma. LIPIcs Proceedings Int. Conf. on Interactive Theorem Proving ITP 2021. Dagstuhl: LiPIcs, 2021. p. 26:1-26:17.
-
da Silveira, Lucas A. ; SONCCO-ALVAREZ, JOSE L. ; DE LIMA, THAYNARA A. ; AYALA-RINCON, MAURICIO . Heterogeneous Parallel Island Models. In: 2021 IEEE Symposium Series on Computational Intelligence (SSCI), 2021, Orlando. 2021 IEEE Symposium Series on Computational Intelligence (SSCI), 2021. p. 1-8.
-
Ayala-Rincón, Mauricio ; Ferreira Silva, G. ; FERNANDEZ, M. ; NANTES-SOBRINHO, DANIELE . A Certified Functional Nominal C-Unification Algorithm - Revised version. In: Logic-Based Program Synthesis and Transformation LOPSTR, 2020, Porto. LNCS Proc. Logic-Based Program Synthesis and Transformation LOPSTR, selected and revised papers. Zurique: Springer Nature Switzerland AG, 2020. v. 12042. p. 123-138.
-
da Silveira, Lucas A. ; SONCCO-ALVAREZ, JOSE L. ; DE LIMA, THAYNARA A. ; AYALA-RINCON, MAURICIO . Behavior of Bioinspired Algorithms in Parallel Island Models. In: 2020 IEEE Congress on Evolutionary Computation (CEC), 2020, Glasgow. 2020 IEEE Congress on Evolutionary Computation (CEC), 2020. p. 1-8.
-
AYALA-RINCON, MAURICIO ; FERNANDEZ, M. ; NANTES-SOBRINHO, DANIELE ; Vale, Deivid . An Investigation into General Nominal Equational Problems. In: 34th International Workshop on Unification UNIF 2020, 2020, Paris. Proc. 34th International Workshop on Unification (UNIF), Temur Kutsia and Andrew M. Marshall (Eds.),. Linz: RISC-Linz Report Series No. 20-10, 2020. v. 20. p. 1-8.
-
M. Ayala-Rincón ; De Lima, T.A. . Teaching Interactive Proofs to Mathematicians. In: 9th International Workshop on Theorem Prover Components for Educational Software (ThEdu'20), 2020, Paris. EPTCS Proc. ThEdu 2020, 2020. p. 1-15.
-
DE BARROS, JESSE BARRETO ; Anantharajaiah, N. ; M. Ayala-Rincón ; LLANOS, C. H. ; BECKER, Jürgen . A Study of the Impact of Formulation of CostFunction in Task Mapping Problem on NoCs. In: IEEE Nordic Circuits and Systems Conference (NorCAS 2020), 2020, Oslo. IEEE Proc. NorCAS 2020. New York: IEEE Xpress, 2020. p. 1-8.
-
M. Ayala-Rincón ; FERNANDEZ, M. ; Ferreira Silva, G. . Formalising Nominal AC-Unification. In: 33rd International Workshop on Unification - UNIF 2019, 2019, Dortmund. Proceedings UNIF 2019. Dortmund: FSCD, 2019. v. 1. p. 1-8.
-
da Silveira, Lucas A. ; SONCCO-ALVAREZ, JOSE L. ; DE LIMA, THAYNARA A. ; AYALA-RINCON, MAURICIO . Parallel Island Model Genetic Algorithms applied in NP-Hard problems. In: 2019 IEEE Congress on Evolutionary Computation (CEC), 2019, Wellington. 2019 IEEE Congress on Evolutionary Computation (CEC), 2019. p. 3262-3269.
-
Ayala-Rincon, M. ; FERNANDEZ, M. ; Ferreira Silva, G. ; NANTES-SOBRINHO, DANIELE . A Certified Functional Nominal C-Unification Algorithm. In: The 29th International Symposium on Logic-based Program Synthesis and Transformation LOPSTR 2019, 2019, Porto. Pré-Proc. LOPSTR 2019, 2019. p. 1-15.
-
ALMEIDA, A. A. ; Ayala-Rincon, M. . Formalizing the Dependency Pair Criterion for Innermost Termination. In: 22nd Brazilian Symposium on Formal Methods SBMF `, 2019, São Paulo. Pre-proceedings SBMF 2019, 2019. p. 1-40.
-
DE BARROS, JESSE BARRETO ; AYALA-RINCON, MAURICIO ; QUINTERO, CARLOS HUMBERTO LLANOS . Application of an Adaptive Genetic Algorithm for Task Mapping Optimisation on a Wormhole-based Real-time Network-on-Chip. In: 2019 IX Brazilian Symposium on Computing Systems Engineering (SBESC), 2019, Natal. 2019 IX Brazilian Symposium on Computing Systems Engineering (SBESC). New York: IEEE Xplore, 2019. p. 1.
-
SAAD NOGUEIRA NUNES, DANIEL ; Louza, Felipe ; GOG, SIMON ; AYALA-RINCON, MAURICIO ; Navarro, Gonzalo . A Grammar Compression Algorithm Based on Induced Suffix Sorting. In: 2018 Data Compression Conference (DCC), 2018, Snowbird. 2018 Data Compression Conference. http://www.cs.brandeis.edu/~dc: IEEE, 2018. p. 42-51.
-
da Silveira, Lucas A. ; Soncco-Álvarez, J.L. ; De Lima, T.A. ; Ayala-Rincon, M. . Parallel Multi-Island Genetic Algorithms for Sorting Unsigned Genomes by Reversals. In: 2018 IEEE Congress on Evolutionary Computation (CEC), 2018, Rio de Janeiro. Proc. 2018 IEEE Congress on Evolutionary Computation (CEC). Danvers: IEEE Xplore, 2018. p. 1-8.
-
M. Ayala-Rincón ; FERNANDEZ, M. ; NANTES-SOBRINHO, DANIELE . Fixed-Point Constraints for Nominal Equational Unification. In: 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), 2018, Oxford. Proc.3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Dagstuhl: Leibniz International Proceedings in Informatics (LIPIcs), 2018. p. 7-1-7-16.
-
M. Ayala-Rincón ; de Carvalho-Segundo, Washington ; FERNANDEZ, M. ; NANTES-SOBRINHO, DANIELE . A Formalisation of Nominal C-Matching through Unification with Protected Variables. In: 13th Logical and Semantic Frameworks with Applications (LSFA), 2018, Fortaleza. Pre-proc. 13th Logical and Semantic Frameworks with Applications. Fortaleza: UFCE, 2018. p. 28-41.
-
Delboni, B. de A. ; M. Ayala-Rincón ; NANTES-SOBRINHO, DANIELE . Topological Graphs and Combinators. In: 13th Logical and Semantic Frameworks with Applications (LSFA), 2018, Fortaleza. Pre-proc. 13th Logical and Semantic Frameworks with Applications. Fortaleza: UFCE, 2018. p. 115-127.
-
Ramos, T. M. F. ; Muñoz, César ; M. Ayala-Rincón ; Moscato, Mariano ; Dutle, Aaron ; Narkawicz, Anthony . Formalization of the Undecidability of the Halting Problem for a Functional Language. In: 25th Workshop on Logic, Language, Information and Computation WoLLIC 2018, 2018, Bogotá. Springer LNCS Proceedings. Berlin, Heidelberg: Springer, 2018. v. 10944. p. 196-209.
-
M. Ayala-Rincón ; de Carvalho-Segundo, Washington ; FERNANDEZ, M. ; NANTES-SOBRINHO, DANIELE . Nominal C-Unification. In: 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2017), 2018, Namur. Springer LNCS Proceedings 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2017). Berlin, Heidelberg: Springer, 2018. v. 10855. p. 235-251.
-
DA SILVEIRA, LUCAS ANGELO ; SONCCO-ALVAREZ, JOSE LUIS ; AYALA-RINCON, MAURICIO . Parallel genetic algorithms with sharing of individuals for sorting unsigned genomes by reversals. In: 2017 IEEE Congress on Evolutionary Computation (CEC), 2017, Donostia. 2017 IEEE Congress on Evolutionary Computation (CEC), 2017. p. 741-748.
-
SONCCO-ALVAREZ, JOSE LUIS ; AYALA-RINCON, MAURICIO . Variable neighborhood search for the large phylogeny problem using gene order data. In: 2017 IEEE Congress on Evolutionary Computation (CEC), 2017, Donostia. 2017 IEEE Congress on Evolutionary Computation (CEC), 2017. p. 59-66.
-
M. Ayala-Rincón ; Dundua, Besik ; Kutsia, T. ; MARIN, M. . Rewriting Logic from a rho-Log Point of View. In: Logical and Semantic Frameworks with Applications, LSFA, 2017, Brasília. Pre-proceedings LSFA 2017, 2017. p. 1-16.
-
Ayala-Rincón, Mauricio ; de Carvalho-Segundo, Washington ; FERNANDEZ, M. ; NANTES-SOBRINHO, DANIELE . On solving nominal fixpoint equations. In: Frontiers on Combining Systems FroCoS 2017, 2017, Brasília. Springer LNAI Proc. Frontiers on Combining Systems FroCoS 2017. Heidelberg: Springer International Publishing, 2017. v. 10483. p. 209-226.
-
da Silveira, Lucas A. ; Soncco-Álvarez, José L. ; Ayala-Rincón, Mauricio . Parallel Memetic Genetic Algorithms for Sorting Unsigned Genomes by Translocations. In: IEEE Congress on Evolutionary Computation (CEC 2016), 2016, Vancouver. IEEE Xplore Proc. CeC 2016, 2016. p. 185-192.
-
M. Ayala-Rincón ; FERNANDEZ, M. ; Sobrinho, Daniele Nantes . Nominal Narrowing. In: International Conference on Formal Structures for Computation and Deduction (FSCD), 2016, Porto. LIPIcs Proceedings Formal Structures for Computation and Deduction (FSCD). Dagstuhl: Leibniz International Proceedings in Informatics (LIPIcs), 2016. v. 52. p. 1-17.
-
M. Ayala-Rincón ; Carvalho Segundo, W.L.R. ; FERNANDEZ, M. ; Sobrinho, Daniele Nantes . A Formalisation of Nominal Alpha-Equivalence with A and AC Function Symbols. In: Logical and Semantic Frameworks with Applications LSFA 2016, 2016, Porto. Pre-proceedings LSFA 2016. Porto: FSCD Satellite event, 2016. p. 78-93.
-
Ramos, T. M. F. ; Ayala-Rincón, Mauricio . Formalization of the Undecidability of the Halting Problem for a Turing Complete Functional Language. In: Escola de Informática Teórica e Métodos Formais (ETMF 2016), 2016, Natal. Anais Escola de Informática Teórica e Métodos Formais (ETMF 2016). Porto Alegre: SBC-UFRN-UFPel, 2016. p. 165-174.
-
Viso, Andres ; Bonelli, Eduardo ; M. Ayala-Rincón . Type Soundness for Path Polymorphism. In: 10th Logical and Semantic Frameworks, with Applications, 2015, Natal. Pré-proceedings 10th Workshop on Logical and Semantic Frameworks with Applications. Natal: UFRN, 2015. p. 3-18.
-
M. Ayala-Rincón ; FERNANDEZ, M. ; Rocha Oliveira, Ana Cristina . Completeness in PVS of a Nominal Unification Algorithm. In: 10th Logical and Semantic Frameworks, with Applications, 2015, Natal. Pré-proceedings 10th Workshop on Logical and Semantic Frameworks with Applications. Natal: UFRN, 2015. p. 19-34.
-
M. Ayala-Rincón ; FERNÁNDEZ, MARIBEL ; Gabbay, Murdoch ; Rocha Oliveira, Ana Cristina . Checking Overlaps in Nominal Rewriting Rules. In: 10th Logical and Semantic Frameworks, with Applications, 2015, Natal. Pré-proceedings 10th Workshop on Logical and Semantic Frameworks with Applications. Natal: UFRN, 2015. p. 199-214.
-
NUNES, D. S. N. ; M. Ayala-Rincón . A Practical Semi-External Memory Method for Approximate Pattern Matching. In: 3º Workshop-Escola de Informática Teórica (WEIT 2015), 2015, Porto Alegre. Proc. WEIT 2015. Porto Alegre: UFRGS, 2015. p. 1-8.
-
da Silveira, Lucas A. ; SONCCO-ALVAREZ, JOSE L. ; DE LIMA, THAYNARA A. ; AYALA-RINCON, MAURICIO . Computing translocation distance by a genetic algorithm. In: 2015 XLI Latin American Computing Conference (CLEI), 2015, Arequipa. 2015 Latin American Computing Conference (CLEI), 2015. p. 1-12.
-
SONCCO-ALVAREZ, JOSE LUIS ; AYALA-RINCON, MAURICIO . Memetic algorithm for sorting unsigned permutations by reversals. In: 2014 IEEE Congress on Evolutionary Computation (CEC), 2014, Beijing. 2014 IEEE Congress on Evolutionary Computation (CEC). p. 2770-8.
-
ALMEIDA, ARIANE ALVES ; LLANOS, CARLOS H. ; ARIAS-GARCÍA, JANIER ; Ayala-Rincón, Mauricio . Verification of Hardware Implementations through Correctness of their Recursive Definitions in PVS. In: the 27th Symposium, 2014, Aracaju. Proceedings of the 27th Symposium on Integrated Circuits and Systems Design - SBCCI '14. New York: ACM Press. p. 1-6.
-
MOURA, Flávio Leonardo Cavalcanti de ; KESNER, Delia ; Ayala-Rincón, Mauricio . Metaconfluence of Calculi with Explicit Substitutions at a Distance. In: 34th Foundations of Software Technology and Theoretical Computer Science conference (FSTTCS), 2014, Nova Deli. LIPIcs IARCS Proceedings 34th Foundations of Software Technology and Theoretical Computer Science conference. Dagsstuhl: Leibniz International Proceedings in Informatics (LIPIcs), 2014. v. 29. p. 391-402.
-
ARIAS-GARCIA, JANIER ; BRAGA, ANDRE ; LLANOS, CARLOS H. ; AYALA-RINCON, MAURICIO ; PEZZUOL JACOBI, RICARDO ; FOLTRAN, ALFREDO . FPGA HIL simulation of a linear system block for strongly coupled system applications. In: 2013 IEEE International Conference on Industrial Technology (ICIT 2013), 2013, Cape Town. 2013 IEEE International Conference on Industrial Technology (ICIT). p. 1017-1022.
-
MUNOZ, DANIEL M. ; LLANOS, CARLOS H. ; DOS SANTOS COELHO, LEANDRO ; AYALA-RINCON, MAURICIO . Hardware-based parallel firefly algorithm for embedded applications. In: 2013 NASA/ESA Conference on Adaptive Hardware and Systems (AHS), 2013, Torino. 2013 NASA/ESA Conference on Adaptive Hardware and Systems (AHS-2013). p. 39-46.
-
Rocha Oliveira, Ana Cristina ; GALDINO, André Luiz ; M. Ayala-Rincón . Synchronizing Applications of the Parallel Moves Lemma to Formalize Confluence of Orthogonal TRSs in PVS. In: 2nd International Workshop on Confluence, IWC 2013, 2013, Eindhoven. Proc. 2nd International Workshop on Confluence IWC 2013. Eindhoven: Rewriting Deduction and Programming 2013 RDP, 2013. p. 47-51.
-
SONCCO-ALVAREZ, JOSE LUIS ; ALMEIDA, GABRIEL MARCHESAN ; BECKER, JUERGEN ; AYALA-RINCON, MAURICIO . Parallelization and virtualization of genetic algorithms for sorting permutations by reversals. In: 2013 World Congress on Nature and Biologically Inspired Computing (NaBIC), 2013, Fargo. 2013 World Congress on Nature and Biologically Inspired Computing. p. 29-35.
-
NUNES, D. S. N. ; M. Ayala-Rincón . A compressed suffix tree based implementation with low peak memory usage. In: Latin American Conference on Informatics CLEI 2013, 2013, Naiguatá. Pré-Proc. - Special Edition 39th Latin American Computer Conference - CLEI 2013. Caracas: CLEI - Universidad Simon Bolivar USB, 2013. p. 72-80.
-
Ayala-Rincón, Mauricio ; MOURA, Flávio Leonardo Cavalcanti de . Computational Deduction and Formal Proofs Logic for Computation that is truly Computational. In: 8th Colombian Conference on Computation - 8CCC, 2013, Armenia. Anais locais 8th CCC. Popayan/Armenia: Universidade del Quindío/Universidade del Cauca, 2013. p. 166-174.
-
ARIAS-GARCIA, J. ; LLANOS, Carlos ; M. Ayala-Rincón ; JACOBI, Ricardo P . A fast and low cost architecture developed in FPGAs for solving systems of linear equations. In: 3rd IEEE Latin American Symposium on Circuits and Systems LASCAS 2012, 2012, Playa del Carmen. IEEE Proc. LASCAS 2012, 2012. p. 1-4.
-
MUNOZ, D. ; LLANOS, Carlos ; Coelho, Leandro ; M. Ayala-Rincón . Accelerating the Artificial Bee Colony Algorithm by Hardware Parallel Implementations. In: 3rd IEEE Latin American Symposium on Circuits and Systems LASCAS 2012, 2012, Playa del Carmen. IEEE Proc. LASCAS 2012, 2012. p. 1-4.
-
ARIAS-GARCIA, J. ; LLANOS, Carlos ; M. Ayala-Rincón ; JACOBI, Ricardo P . 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, Bento Gonçalves. IEEE Proc. SPL 2012, 2012. p. 1-6.
-
AYALARINCON, M . Reusing Formal Proofs Through Isomorophisms (Paper of Invited Talk). In: Requirements Engineering and Software Testing LA Congress, 2012, Medellín. Proc. LACREST Requirements Engineering and Software Testing. Medellín: Instituto Antioqueño de Investigación, 2012. p. 140-146.
-
DE LIMA, THAYNARA ARIELLY ; AYALA-RINCON, MAURICIO . Complexity of Cayley distance and other general metrics on permutation groups. In: 2012 7th Colombian Computing Congress (CCC), 2012, Medellin. 2012 7th Colombian Computing Congress (CCC), 2012.
-
SONCCO-ALVAREZ, JOSE LUIS ; AYALA-RINCON, MAURICIO . A genetic approach with a simple fitness function for sorting unsigned permutations by reversals. In: 2012 7th Colombian Computing Congress (CCC), 2012, Medellin. 2012 7th Colombian Computing Congress (CCC).
-
Ayala-Rincón, Mauricio ; FERNANDEZ, M. ; NANTES-SOBRINHO, DANIELE . Elementary Deduction Problem for Locally Stable Theories with Normal Foms. In: Logical and Semantic Frameworks with Applications LSFA 2012, 2012, Rio de Janeiro/Niteroi. Pré-proceedings VII Workshop on Logical and Semantic Frameworks with Applications. UFF Niteroi: Booklet edited by Delia Kesner and Petrucio Viana, 2012. p. 35-49.
-
ARIAS-GARCIA, J. ; JACOBI, Ricardo P ; LLANOS, Carlos ; Ayala-Rincón, Mauricio . A Suitable FPGA Implementation of Floating-Point Matrix Inversion based on Gauss-Jordan Elimination. In: VII Southern Conference on Programmable Logic (SPL 2011), 2011, Cordoba. IEEE Proc. VII Southern Conference on Programmable Logic (SPL 2011), 2011. p. 263-268.
-
MUNOZ, D. ; LLANOS, Carlos ; Coelho, Leandro ; Ayala-Rincón, Mauricio . Hardware Particle Swarm Optimization with Passive Congregation for Embedded Applications. In: VII Southern Conference on Programmable Logic (SPL 2011), 2011, Cordoba. IEEE Proc. VII Southern Conference on Programmable Logic (SPL 2011), 2011. p. 173-178.
-
MUNOZ, D. ; LLANOS, Carlos ; Coelho, Leandro ; M. Ayala-Rincón . Opposition-based Shuffled PSO with Passive Congregation Applied to FM Matching Synthesis. In: 2011 IEEE Congress on Evolutionary Computation (2011 IEEE CeC), 2011, New Orleans. IEEE Proc. Congress on Evolutionary Computation (2011 IEEE CeC), 2011. p. 2775-2781.
-
Ventura, Daniel ; Ayala-Rincón, Mauricio ; KAMAREDDINE, Fairouz . Principal Typings in a Restricted Intersection Type System for Beta Normal Forms with De Bruijn Indices. In: 9th International Workshop on Reduction Strategies in Rewriting and Programming, 2010, Brasília. Electronic Proceedings in Theoretical Computer Science. Sydney: EPTCS. v. 15. p. 69-82.
-
MUNOZ, D. ; SANCHEZ, D. F. ; LLANOS, Carlos ; M. Ayala-Rincón . FPGA based floating-point library for CORDIC algorithms. In: IEEE Proc. VI Southern Programmable Logic Conference SPL 2010, 2010, Porto de Galinhas. IEEE Proceeding of the VI Southern Programmable Logic Conference SPL 2010, 2010. p. 55-60.
-
NOGUEIRA, R. B. ; Nascimento, A. ; MOURA, Flávio Leonardo Cavalcanti de ; Ayala-Rincón, Mauricio . Formalization of Security Proofs Using PVS in the Dolev-Yao Model. In: 6th Computability in Europe - Programs, Proofs and Processes CiE 2010, 2010, Azores. Proc. Computability in Europe - Programs, Proofs and Processes (Booklet) CiE 2010, 2010. p. 1-12.
-
VENTURA, Daniel Lima ; KAMAREDDINE, Fairouz ; Ayala-Rincón, Mauricio . Intersection type systems and explicit substitutions calculi. In: 17th Workshop on Logic, Language, Information and Computation, 2010, Brasília. Springer LNCS Proc. 17th Workshop on Logic, Language, Information and Computation. Heidelberg: Springer-Verlag, 2010. v. 6188. p. 232-246.
-
Avelar, Andréia B ; MOURA, Flávio Leonardo Cavalcanti de ; GALDINO, André Luiz ; Ayala-Rincón, Mauricio . Verification of The Completeness of Unification Algorithms à la Robinson. In: 17th Workshop on Logic, Language, Information and Computation, 2010, Brasília. Springer LNCS Proc. 17th Workshop on Logic, Language, Information and Computation. Heidelberg: Springer-Verlag, 2010. v. 6188. p. 110-124.
-
Sobrinho, Daniele Nantes ; Ayala-Rincón, Mauricio . Reduction of the intruder deduction problem into equational elementary deduction for electronic purse protocols with blind signatures. In: 17th Workshop on Logic, Language, Information and Computation, 2010, Brasília. Springer LNCS Proc. 17th Workshop on Logic, Language, Information and Computation. Heidelberg: Springer-Verlag, 2010. v. 6188. p. 218-231.
-
MUNOZ, D. ; LLANOS, Carlos ; Coelho, Leandro ; M. Ayala-Rincón . Accelerating the Shuffled Frog Leaping algorithm by parallel implementations in FPGAs. In: The IEEE Fifth International Conference on Bio-Inspired Computing: Theories and Applications (BIC-TA 2010), 2010, Liverpool. Proc. of the IEEE Fifth International Conference on Bio-Inspired Computing: Theories and Applications (BIC-TA 2010), 2010. p. 1526-1531.
-
MUNOZ, D. ; LLANOS, Carlos ; Coelho, Leandro ; M. Ayala-Rincón . Comparison Between two FPGA Implementations of the Particle Swarm Optimization Algorithm for High-performance Embedded Applications. In: The IEEE Fifth International Conference on Bio-Inspired Computing: Theories and Applications (BIC-TA 2010), 2010, Liverpool. Proc. of the IEEE Fifth International Conference on Bio-Inspired Computing: Theories and Applications (BIC-TA 2010), 2010. p. 1637-1642.
-
ARBOLEDA, Daniel Muñoz ; LLANOS, Carlos ; M. Ayala-Rincón ; Coelho, Leandro . Hardware Particle Swarm Optimization based on the Attractive-Repulsive Scheme for Embedded Applications. In: International Conference on ReConFigurable Computing and FPGAs ReConFig 2010, 2010, Cancun. Proc. International Conference on ReConFigurable Computing and FPGAs, 2010. p. 1-6.
-
SANCHEZ, D. F. ; MUNOZ, D. ; LLANOS, Carlos ; M. Ayala-Rincón . Parameterizable Floating-point Library for Arithmetic Operations in FPGAs. In: 22nd Symposium on Integrated Circuits and System Design - SBCCI 09, 2009, Natal. ACM Proc. 22nd Symposium on Integrated Circuits and System Design - SBCCI 09, 2009. p. 40-46.
-
MUNOZ, D. ; LLANOS, Carlos ; Coelho, Leandro ; Ayala-Rincon, M. . Hardware Architecture for Particle Swarm Optimization Using Floating-Point Arithmetic. In: Ninth International Conference on Intelligent Systems Design and Applications (ISDA'09), 2009, Pisa (Itália). IEEE Proceedings 9th Int. Conference on Intelligent Systems Design and Applications ISDA 2009. USA: IEEE Computer Society, IEEE Xexpress, 2009. p. 243-248.
-
MUNOZ, D. ; LLANOS, Carlos ; Coelho, Leandro ; Ayala-Rincón, Mauricio . Elevator Systems with Destination Control and FPGA Implementation of Dispatching Algorithms. In: 20th International Congress of Mechanical Engineering COBEM, 2009, Gramado. Proc. ABCM 20th International Congress of Mechanical Engineering, 2009. p. 1-10.
-
VENTURA, Daniel Lima ; M. Ayala-Rincón ; KAMAREDDINE, Fairouz . Principal Typing for Explicit Substitutions Calculi. In: 4th Conference on Computability in Europe (CiE 2008), 2008, Atenas. Springer-Verlag LNCS, Proc. Logic and Theory of Algorithms, Fourth Conference on Computability in Europe, 2008. v. 5028. p. 567-578.
-
LLANOS, Carlos ; ARBOLEDA, Daniel Muñoz ; M. Ayala-Rincón ; van ELS, R. . FPGA Implementation of Dispatching Algorithms for Local Control of Elevator Systems. In: IEEE International Symposium on Industrial Electronics ? ISIE 2008, 2008, Cambridge. Proc. IEEE International Symposium on Industrial Electronics ? ISIE 2008, 2008. p. 1997-2002.
-
GALDINO, André Luiz ; M. Ayala-Rincón . Verification of Newman's and Yokouchi's Lemmas in PVS. In: Computability in Europe 2008 Logic and Theory of Algorithms CiE 2008, 2008, Atenas. Pre-proceedings volume CiE 2008, 2008.
-
GALDINO, André Luiz ; Cesar Munoz ; M. Ayala-Rincón . Formal Verification of an Optimal Air Traffic Conflict Detection and Recovery Algorithm. In: 14th International Workshop on Logic, Language, Information and Computation - WoLLIC 2007, 2007, Rio de Janeiro. Springer-Verlag LNCS, Proc. 14th International Workshop on Logic, Language, Information and Computation - WoLLIC 2007. Berlin: Springer-Verlag, 2007. v. 4576. p. 177-188.
-
VENTURA, Daniel Lima ; M. Ayala-Rincón ; KAMAREDDINE, Fairouz . Principal Typing for Explicit Substitutions Calculi. In: 4th International Workshop on Higher-Order Rewriting, 2007, Paris. Proc. 4th International Workshop on Higher-Order Rewriting - HOR 2007. Paris: RDP, 2007.
-
GALDINO, André Luiz ; M. Ayala-Rincón . A PVS theory for abstract rewriting systems. In: XXXIII Conferencia Latinoamericana de Informática, 2007, San José. Memorias de la XXXIII Conferencia Latinoamericana de Informática. San José: CLEI, 2007. p. 1-16.
-
M. Ayala-Rincón ; SANT'ANA, Thomas Mailleux . SAEPTUM: Verification of ELAN Hardware Specifications using the Proof Assistant PVS. In: 19th Symposium on Integrated Circuits and System Design - SBCCI 06, 2006, Ouro Preto. ACM Proc. SBCCI 2006. New York: ACM Press, 2006. p. 125-130.
-
LLANOS, Carlos ; ARBOLEDA, Daniel Muñoz ; M. Ayala-Rincón . Implementation of Dispatching Algorithms for Elevator Systems using Reconfigurable Architectures. In: 19th Symposium on Integrated Circuits and System Design - SBCCI 06, 2006, Ouro Preto. ACM Proc. SBCCI 2006. New York: ACM Press, 2006. p. 32-37.
-
ARBOLEDA, Daniel Muñoz ; LLANOS, Carlos ; M. Ayala-Rincón . Implementation, Simulation and Validation of Dispatching Algorithms for Elevator Systems. In: International Conference on Reconfigurable Computing and FPGAs 2006 - ReConFig'06, 2006, San Luís Potosí. IEEE CS Proc. Third Int. conf. on Reconfigurable Computing and FPGAs 2006. Los Alamitos CA USA: IEEE CS, 2006. p. 1-8.
-
VENTURA, Daniel Lima ; M. Ayala-Rincón ; KAMAREDDINE, Fairouz . Explicit Substitutions Calculi with Explicit Eta rules which Preserve Subject Reduction. In: Brazilian Workshop on Logical and Semantic Frameworks, with Applications, 2006, Natal. Proc. Brazilian Workshop on Logical and Semantic Frameworks, with Applications. Natal: SBC/UFRN, 2006. p. 1-15.
-
MOURA, Flávio Leonardo Cavalcanti de ; KAMAREDDINE, Fairouz ; M. Ayala-Rincón . Second-Order Matching via Explicit Substitutions. In: Eleventh International Conference on Logic for Programming Artificial Intelligence and Reasoning - LPAR, 2005, Montevideo. Proc. Eleventh Int. Conf. on Logic for Programming Artificial Intelligence and Reasoning - LPAR, Springer-Verlag LNAI (LNCS). Berlin/Heidelberg: Springer Verlag, 2005. v. 3452. p. 433-448.
-
BOUKERCHE, Azzedine ; MELO, Alba Cristina Magalhaes Alves de ; M. Ayala-Rincón ; WALTER, Maria Emilia Machado Telles ; SANT'ANA, Thomas Mailleux . Parallel Strategies for Local Biological Sequence Alignment in a Cluster de Workstations. In: Fourth Workshop on Performance, Modeling, Evaluation and Optimization of Parallel and Distribuited Systems (PMEO-PDS 2005), 2005, Denver. Proceedings of the 19th International Parallel & Distribuited Processing Symposium (IPDPS 2005). Los Alamos: IEEE, 2005. p. 268b-275.
-
MOURA, Flávio Leonardo Cavalcanti de ; M. Ayala-Rincón ; KAMAREDDINE, Fairouz . SUBSEXPL: a Tool for Simulating and Comparing Explicit Substitutions Calculi. In: 5th International Workshop on the Implementation of Logics (in conjunction with LPAR 2004), 2005, Montevideo. Proc. 5th International Workshop on the Implementation of Logics, 2005. p. 16-30.
-
BOUKERCHE, Azzedine ; MELO, Alba Cristina Magalhaes Alves de ; M. Ayala-Rincón ; SANT'ANA, Thomas Mailleux . Parallel Smith-Waterman Algorithm for Local DNA Comparison in a Cluster of Workstations. In: Experimental and Efficient Algorithms: 4th Int. WEA 2005, 2005, Santorini Island. Experimental and Efficient Algorithms, Springer-Verlag LNCS. Berlin/Heidelberg: Springer-Verlag, 2005. v. 3503. p. 464-475.
-
MORRA, Carlos ; BECKER, Jürgen ; M. Ayala-Rincón ; HARTENSTEIN, Reiner W . FELIX: Using Rewriting-Logic for Generating Functionally Equivalent Implementations. In: 15th Field-Programmable Logic and Applications - FPL 2005, 2005, Tampere. IEEE CS Proc. 15th International Conference, Field-Programmable Logic and Applications. Tampere: IEEE, 2005. p. 25-30.
-
BRAGA, André ; LLANOS, Carlos ; M. Ayala-Rincón ; JACOBI, Ricardo P . VANNGen: a Flexible CAD Tool for Hardware Implementation of Artificial Neural Networks. In: International Conference on Reconfigurable Computing and FPGAs 2005 - ReConFig'05, 2005, Puebla. IEEE CS Proc. Int. Conf. on Reconfigurable Computing and FPGAs - ReConFig05, 2005. p. 1-8.
-
SANT'ANA, Thomas Mailleux ; M. Ayala-Rincón . Verification of Rewrite Based Specifications Using Proof Assistants. In: XXXI Conf. Latinoamericana de Informática CLEI2005, 2005, Cali. Proc. XXXI Conf. Latinoamericana de Informática - CLEI2005, 2005. p. 699-710.
-
MIRANDA, Rodrigo César de Castro ; M. Ayala-Rincón . A Modification of the Landau-Viskin Algorithm Computing Longest Common Extensions Using Suffix Arrays. In: XXXI Conf. Latinoamericana de Informática CLEI2005, 2005, Cali. Proc. XXXI Conf. Latinoamericana de Informática CLEI2005, 2005. p. 41-50.
-
SANDES, Edans Flávius de Oliveira ; MELO, Alba Cristina Magalhaes Alves de ; M. Ayala-Rincón . Comparação Paralela Exata de Sequências Biológicas Longas em Clusters de Computadores. In: 4th International Information and Telecommunication Technologies Symposium, 2005, Florianópolis. Proc. 4th International Information and Telecommunication Technologies Symposium, 2005. p. 1-8.
-
AYALA-RINC'N, MAURICIO ; JACOBI, RICARDO P. ; CARVALHO, LUIS G. A. ; LLANOS, CARLOS H. ; HARTENSTEIN, REINER W. . Modeling and prototyping dynamically reconfigurable systems for efficient computation of dynamic programming methods by rewriting-logic. In: the 17th symposium, 2004, Pernambuco. Proceedings of the 17th symposium on Integrated circuits and system design - SBCCI '04. New York: ACM Press. p. 248-253.
-
LLANOS, Carlos ; JACOBI, Ricardo P ; M. Ayala-Rincón ; HARTENSTEIN, Reiner W . A Dynamically Reconfigurable System for Space-Efficient Computation of the FFT. In: International Conference on Reconfigurable Computing and FPGAs 2004 - ReConFig'04, 2004, Colima. Proc. International Conference on Reconfigurable Computing and FPGAs 2004 - ReConFig'04. México: Sociedad Mexicana de Computación, 2004. p. 360-369.
-
JACOBI, Ricardo P ; M. Ayala-Rincón ; CARVALHO, Luis G A ; LLANOS, Carlos ; HARTENSTEIN, Reiner W . Reconfigurable Systems for Sequence Alignment and for General Dynamic Programming. In: Third Brazilian Workshop on Bioinformatics, 2004, Brasília. Proc. Third Brazilian Workshop on Bioinformatics - WOB 2004, 2004. p. 25-32.
-
M. Ayala-Rincón ; NOGUEIRA, R. B. ; JACOBI, Ricardo P ; LLANOS, Carlos ; HARTENSTEIN, Reiner W . Modeling a Reconfigurable System for Computing the FFT in Place via Rewriting-Logic. In: 16th Symposium on Integrated Circuits and System Design - SBCCI 03, 2003, São Paulo. Proc. 16th Symposium on Integrated Circuits and System Design - SBCCI 03, 2003. p. 205-210.
-
HARTENSTEIN, Reiner W ; JACOBI, Ricardo P ; M. Ayala-Rincón ; LLANOS, Carlos . Using Rewriting-Logic Notation for Funcional Verification in Data-Stream Based Reconfigurable Computing. In: Forum on Specification and Design Languages - FDL 03, 2003, Frankfurt. Proc. Forum on Specification and Design Languages - FDL 03. Brusselas: European Chips and Systems Initiative (ECSI), 2003. p. 1-10.
-
M. Ayala-Rincón ; NOGUEIRA, R. B. ; LLANOS, Carlos ; JACOBI, Ricardo P ; HARTENSTEIN, Reiner W . Efficient Computation of Algebraic Operations over Dynamically Reconfigurable Systems Specified by Rewriting-Logic Environments. In: XXIII International Conference of the Chilean Computer Science Society, 2003, Chillán. Proc. 23rd International Conf. of the Chilean Computer Science Society, 2003. p. 60-69.
-
M. Ayala-Rincón ; MOURA, Flávio Leonardo Cavalcanti de ; KAMAREDDINE, Fairouz . Comparing Calculi of Explicit Substitutions with Eta-Reduction. In: Ninth Workshop on Logic, Language, Information and Computation - WoLLIC 2002, 2002, Rio de Janeiro. Proc. Ninth Workshop on Logic, Language, Information and Computation. Amsterdam: Elsevier ENTCS, 2002. v. 67. p. 77-96.
-
KAMAREDDINE, Fairouz ; MONIN, François ; M. Ayala-Rincón . On automating the extraction of programs from proofs using product types. In: Ninth Workshop on Logic, Language, Information and Computation - WoLLIC 2002, 2002, Rio de Janeiro. Proc. Ninth Workshop on Logic, Language, Information and Computation. Amsterdam: Elsevier ENTCS, 2002. v. 67. p. 215-234.
-
Ayala-Rincón, Mauricio ; NETO, R. M. ; JACOBI, R. P. ; HARTENSTEIN, Reiner W ; LLANOS, C . Applying ELAN Strategies in Simulating Processors over Simple Architectures. In: Second International Wokshop on Reduction Strategies in Rewriting and Programming, 2002, Copenhagen. Proc. Second International Wokshop on Reduction Strategies in Rewriting and Programming. Viena: Verlag Berger, 2002. p. 127-141.
-
M. Ayala-Rincón ; KAMAREDDINE, Fairouz . On Applying the Lambda s_e -Style of Unification for Simply-Typed Higher Order Unification in the Pure lambda Calculus. In: Eighth Workshop on Logic, Language, Information and Computation - WoLLIC 2001, 2001, Brasília. Pré-Proc. Eighth Workshop on Logic, Language, Information and Computation - WoLLIC 2001. Brasília D.F.: CESPE/UnB, 2001. p. 41-53.
-
M. Ayala-Rincón ; GADELHA, L. M. R. . An Efficient Strategy for Word Cycle Completion of Finitely Presented Groups. In: XXI International Conference of the Chilean Computer Science Society, 2001, Punta Arenas. Proc. XXI International Conference of the Chilean Computer Science Society. Los Alamitos, CA USA: IEEE CS press, 2001. p. 80-85.
-
M. Ayala-Rincón ; KAMAREDDINE, Fairouz . Strategies for Simply-Typed Higher Order Unification via lambda s_e-Style of Explicit Substitution. In: The Third International Workshop on Explicit Substitutions Theory and Applications to Programs and Proofs (WESTAPP 2000), 2000, Norwich. WESTAPP 2000 The Third International Workshop on Explicit Substitutions: Theory and Applications to Programs and Proofs. Norwich: University of East Anglia, 2000. p. 3-18.
-
M. Ayala-Rincón ; KAMAREDDINE, Fairouz . Unification via lambda s_e-Style of Explicit Substitution. In: International Conference on Principles and Practice of Declarative Programming (PPDP 2000), 2000, Montreal. Proc. 2nd International Conference on Principles and Practice of Declarative Programming, 2000. p. 163-174.
-
M. Ayala-Rincón ; ARAÚJO, I. E. T. . An Algorithm For General Unification Modulo Presburger Arithmetic. In: Primeir Workshop brasileiro de métodos formais, 1998. Anais Workshop Brasileiro de Métodos Formais. p. 146-151.
-
M. Ayala-Rincón ; CONEJO, P. D. . A Linear Time Lower Bound On Updating Algorithms For Suffix Trees. In: String processing and information retrieval: a south american symposium, 1998. String processing and information retrieval, IEEE Computer Society. Santa Cruz de la Sierra, Boliv: IEEE Computer Press. p. 1-6.
-
M. Ayala-Rincón . Church-Rosser Property for Conditional Rewriting Systems with Built-in Predicates. In: Second International Workshop on Frontiers of Combining Systems, 1998, Amsterdam. Frontiers of Combining Systems ´ 98, 1998. p. 1-21.
-
M. Ayala-Rincón ; GADELHA, L. . Applications Of Decision Algorithms For Presburger Arithmetic In Rewrite Automated Deduction. In: XXIII Latin American Conference on Informatics, 1997. Anais XXIII Latin American Conference on Informatics. Valparaíso, Chile. p. 599-608.
-
M. Ayala-Rincón . A Decision Procedure For Conditional Rewriting Systems With Built-In Predicates. In: XXIV seminário integrado de software e hardware, 1997. Anais do XXIV Seminário integrado de Software e Hardware. Brasília, Brasil. p. 387-398.
-
M. Ayala-Rincón . Transforming CRSs Into TRSs - About Elimination Of The Conditions -. In: XXII Latin American Conference on Informatics, 1996. Proc. XXII Latin American conference on informatics. Bogotá, Colômbia. p. 322-334.
-
M. Ayala-Rincón . A Deductive Calculus For Conditional Equational Systems With Built-In Predicates As Premises - Extended Abstract -. In: XV Int. conference of the Chilean computer science society, 1995. Proc. XV International Conference of the Chilean Computer Science Society. Arica, Chile. p. 25-36.
-
M. Ayala-Rincón . Confluence Of Term Rewriting Systems Under Joinability Of Critical Pairs In One Step Of Parallel Reduction. In: XXII SEMISH / XXI PANEL, 1995. Anais XXII Seminário Integrado de Software e Hardware / XXI Latin American Conference on Informatics. Gramado, Brasil. p. 165-176.
-
M. Ayala-Rincón . Confluence Of Conditional Rewriting Systems With Built-In Predicates As Conditions. In: XXI SEMISH, 1994. Anais do XXI Seminário Integrado de Software e Hardware. Caxambú, Brasil. p. 507-521.
-
Rocha Oliveira, Ana Cristina ; FERNANDEZ, M. ; M. Ayala-Rincón . Formalising the Completeness of a Nominal Unification Algorithm. In: 29th International Workshop on Unification UNIF 2015, 2015, Varsovia. Proc. 29th International Workshop on Unification - UNIF 2015. Paris: Proc. UNIF (U. Paris Diderot http://www.pps.univ-paris-diderot.fr/~treinen/unif/past/index.html), 2015. p. 27-31.
-
De Lima, T.A. ; Ayala-Rincón, Mauricio . On the average reversal distance to sort signed permutations. In: 11th Permutation Patterns, 2013, Paris. 11th Permutation Patterns - Permutation Patterns'13. Paris: U. Paris Diderot, 2013. p. 1-2.
-
NUNES, D. S. N. ; M. Ayala-Rincón . A compressed suffix array based index with succinct longest common prefix information. In: 2012 Brazilian Symposium on Bioinformatics (BSB 2012), 2012, Campo Grande. Brazilian Symposium on Bioinformatics BSB/EBB2012 Digital Proceedings, 2012. p. 1-6.
-
Rocha Oliveira, Ana Cristina ; Ayala-Rincón, Mauricio . Formalizing the Confluence of Orthogonal Rewriting Systems. In: Logical and Semantic Frameworks with Applications LSFA 2012, 2012, Rio de Janeiro/Niteroi. Pré-proceedings VII Workshop on Logical and Semantic Frameworks with Applications. UFF Niteroi: Booklet edited by Delia Kesner and Petrucio Viana, 2012. p. 142-146.
-
ARBOLEDA, Daniel Muñoz ; SANCHEZ, D. F. ; LLANOS, Carlos ; AYALARINCON, M . Tradeoff of FPGA Design of Floating-point Transcendental Functions. In: 17th IFIP/IEEE International Conference On Very Large Scale Integration VLSI-SoC 2009, 2009, Florianópolis. IEEE proc. 17th International Conference On Very Large Scale Integration, 2009. p. 239-242.
-
MIRANDA, Rodrigo César de Castro ; M. Ayala-Rincón . A Modification of the Landau-Vishkin Algorithm Computing Longest Common Extensions via Suffix Arrays - Extended Abstract -. In: Brazilian Simposium on Bioinformatics, 2005, São Leopoldo (SP). Advances in Bioinformatics and Computational Biology, Springer-Verlag LNCS (LNBI). Berlin/Heidelberg: Springer-Verlag, 2005. v. 3594. p. 210-213.
-
Ayala-Rincon, M. ; Sobrinho, Daniele Nantes ; FERNANDEZ, M. . Decidability of Elementary Deduction for Locally Stable Theories with Inverses. In: EBL 2014 - 17th Brazilian Logic Conference, 2014, Petropolis. Anais EBL 2014. Niteroi: SBL-UFF, 2014. p. 1-1.
-
Rocha Oliveira, Ana Cristina ; FERNANDEZ, M. ; Ayala-Rincón, Mauricio . Specification of Nominal terms in PVS. In: EBL 2014 - 17th Brazilian Logic Conference, 2014, Petropolis. Anais EBL 2014. Niteroi: SBL-UFF, 2014. p. 1-1.
-
MOURA, Flávio Leonardo Cavalcanti de ; KESNER, Delia ; Ayala-Rincón, Mauricio . Metaconfluence of Explicit Substitutions Calculi at a Distance. In: EBL 2014 - 17th Brazilian Logic Conference, 2014, Petropolis. Anais EBL 2014. Niteroi: SBL-UFF, 2014. p. 1-1.
-
VENTURA, Daniel Lima ; M. Ayala-Rincón ; KAMAREDDINE, Fairouz . Intersection types and explicit substitution. In: 15th Latin American Symposium on Mathematical Logic SLALM, 2012, Bogotá. Proc. 15th Latin American Symposium on Mathematical Logic SLALM. Bogotá: Universidad de Los Andes, 2012. p. 53-53.
-
Santos Rego, Yuri ; Ayala-Rincón, Mauricio . Formalization of balancing properties using PVS in Dolev and Yao?s cascade protocols model. In: Brazilian Logic Conference, 2011, Petrópolis. Abstracts 16th Brazilian Logic Conference. Petrópolis: LNCC, 2011. p. 52-52.
-
VENTURA, Daniel Lima ; Ayala-Rincón, Mauricio ; KAMAREDDINE, Fairouz . Towards the characterisation of termination for explicit substitution calculi with de Bruijn indices. In: Brazilian Logic Conference, 2011, Petrópolis. Abstracts 16th Brazilian Logic Conference. Petrópolis: LNCC, 2011. p. 66-66.
-
Ayala-Rincón, Mauricio ; Rocha Oliveira, Ana Cristina . On the formalization of confluence of orthogonal rewriting systems in PVS. In: Brazilian Logic Conference, 2011, Petrópolis. Abstracts 16th Brazilian Logic Conference. Petrópolis: LNCC, 2011. p. 31-31.
-
VENTURA, Daniel Lima ; AYALARINCON, M ; KAMAREDDINE, Fairouz . Intersection Type Systems with de Bruijn Indices. In: XV Encontro Brasileiro de Lógica / XIV Simpósio Latino Americano de Lógica Matemática XV EBL / XIV SLALM, 2008, Paratí. Proc. XV Encontro Brasileiro de Lógica / XIV Simpósio Latino Americano de Lógica Matemática XV EBL / XIV SLALM, 2008.
-
MOURA, Flávio Leonardo Cavalcanti de ; M. Ayala-Rincón ; KAMAREDDINE, Fairouz . Higher Order Unification: A structural relation between Huet´s method and the one based on explicit substitutions. In: XIV Encontro Brasileiro de Lógica, 2006, Itatiaia. Caderno de resumos EBL XIV Encontro Brasileiro de Lógica. Campinas: Sociedade Brasileira de Lógica, 2006. p. 1-2.
-
MOURA, Flávio Leonardo Cavalcanti de ; M. Ayala-Rincón ; KAMAREDDINE, Fairouz . Third Order Matching via Explicit Substitutions. In: XIV Encontro Brasileiro de Lógica, 2006, Itatiaia. Caderno de resumos EBL XIV Encontro Brasileiro de Lógica. Campinas: Sociedade Brasileira de Lógica, 2006. p. 1-2.
-
FERREIRA, Hélio Carneiro ; M. Ayala-Rincón . On Combining Beta-Contractions in Calculi of Explicit Substitutions. In: XIV Encontro Brasileiro de Lógica, 2006, Itatiaia. Caderno de Resumos XIV Encontro Brasileiro de Lógica. Campinas: Sociedade Brasileira de Lógica, 2006. p. 1-2.
-
M. Ayala-Rincón ; MOURA, Flávio Leonardo Cavalcanti de ; KAMAREDDINE, Fairouz . Animation of Reduction in the Lambda Calculus and in Calculi of Explicit Substitutions. In: Congresso da Sociedade Brasileira de Matemática Aplicada e Computacional - XXVI CNMAC, 2003, São José do Rio Preto. Anais do XXVI CNMAC. São José do Rio Preto: IBILCE/UNESP, 2003. p. 608-608.
-
M. Ayala-Rincón ; POUBEL, Haydée Werneck ; NOGUEIRA, R. B. . Visualizing Equivalence Relations Between Computational Models and Grammars of Context-Free Languages. In: Congresso da Sociedade Brasileira de Matemática Aplicada e Computacional - XXVI CNMAC, 2003, São José do Rio Preto. Anais XXVI CNMAC. São José do Rio Preto: IBILCE/UNESP, 2003. p. 609-609.
-
M. Ayala-Rincón ; FONSECA, A. F. ; POUBEL, Haydée Werneck ; SIQUEIRA, José de ; SILVA, A. H. R. . Animação de Teoremas de Equivalência entre Autômatos Finitos e Formas Gramaticais de Linguagens Formais. In: XXIV Congresso Nacional de Matemática Aplicada e Computacional, 2001, Belo Horizonte. Anais do XXIV Congresso Nacional de Matemática Aplicada e Computacional, 2001. v. II. p. 365-365.
-
M. Ayala-Rincón ; ARAÚJO, I. E. T. . Unification Problems in Monoidal Theories and Presburger Arithmetic. In: 12th International Workshop on Unification (UNIF98), 1998, Roma. Proceedings 12th International Workshop on Unification, 1998.
-
M. Ayala-Rincón ; GADELHA, L. M. R. . Métodos de Decisão para a Aritmética de Presburger na Dedução Automática com Técnicas de Reescrita. In: XX Congresso Nacional de Matemática Aplicada e Computacional, 1997, Gramado. Resumos XX Congresso Nacional de Matemática Aplicada e Computacional, 1997. p. 392-393.
-
M. Ayala-Rincón ; GADELHA, L. M. R. . Aplicação de Métodos de Programação Linear Inteira para Decisão na Teoria da Aritmética de Presburger. In: XIX Congresso Nacional de Matemática Aplicada e Computacional, 1996, Goiânia. XIX Congresso Nacional de Matemática Aplicada e Computacional, 1996. p. 400-4001.
-
M. Ayala-Rincón . A Note on Confluence of Term Rewriting Systems under Joinability of Critical Pairs in One Step of Parallel Reduction. Bulletin of the European Association for Theoretical Computer Science , v. 58, p. 225-225, 1996.
-
M. Ayala-Rincón . A Deductive Calculus for Conditional Equational Systems with Built-in Predicates - Abstract. Bull. of Symbolic Logic , v. 2, n.2, p. 236-236, 1996.
-
M. Ayala-Rincón . Embedding Built-in Predicates as Premises of Rules of Conditional Rewriting Systems. Journal of the Interest Group in Pure and Applied Logics , v. 4, n.2, p. 309-309, 1996.
-
M. Ayala-Rincón . Expressivenes of Conditional Equational Systems with Built-in Predicates. Bulletin of the European Association for Theoretical Computer Science , v. 53, p. 485-486, 1994.
-
Ayala-Rincon, M. . Palestra convidada (20 años FCEN/UNAL Manizales) 'Verificación Computacional de la Antiunificación Algebraica'. 2025. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincon, M. . Palestra Convidada (Coloquio de Matemáticas, Uniandes) 'Antiunificación Modulo Teorias Equacionales'. 2025. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincon, M. . Guest talk 'Coputational Verification of Anti-Unification' RISC Forum Johannes Kepler Universität Linz. 2025. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Invited Talk 'The Algebra Library and Applications of Quaternions' PVS Day - Workshop on the Prototype Verification System. 2025. (Apresentação de Trabalho/Conferência ou palestra).
-
M. Ayala-Rincón . Invited Talk (Libraries of Digital Math - HIM Trimester Prospects of Formal Mathematics) Formalisation of nominal equational reasoning in PVS: nominal Unification. 2024. (Apresentação de Trabalho/Congresso).
-
M. Ayala-Rincón . Invited Talk (Hausdorff Trimester Program: Prospects of Formal Mathematics) 'Formalisation of nominal equational reasoning in PVS: nominal Anti-Unification'. 2024. (Apresentação de Trabalho/Conferência ou palestra).
-
M. Ayala-Rincón . Invited Talk (EuroProofNet 2024) Verifying Nominal Equational Reasoning Modulo Algorithms - 2nd Workshop on the development, maintenance, refactoring and search of large libraries of proofs. 2024. (Apresentação de Trabalho/Congresso).
-
Ayala-Rincón, Mauricio . Guest talk (RISC Forum/Johannes Kepler Universität Linz) 'Mechanizing Combinatorial Applications of Compactness'. 2024. (Apresentação de Trabalho/Conferência ou palestra).
-
M. Ayala-Rincón . Invited Talk (24th LPAR) 'Formalizing Algebraic Theorems in PVS' 24th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning - LPAR 2023. 2023. (Apresentação de Trabalho/Conferência ou palestra).
-
De Lima, T.A. ; M. Ayala-Rincón . Intensive 10 hours Course (Universidad Nacional de Colombia - Manizales) 'Mechanizing Mathematics'. 2023. (Apresentação de Trabalho/Outra).
-
M. Ayala-Rincón . Invited Talk (37th UNIF) 'Formalisation of Nominal Equational Reasoning' 37th International Workshop on Unification. 2023. (Apresentação de Trabalho/Conferência ou palestra).
-
De Lima, T.A. ; Ayala-Rincon, M. . Short course (6h, collocated with XIV Summer Workshop on Mathematics): Formalizing Theorems with PVS. 2022. (Apresentação de Trabalho/Outra).
-
Ayala-Rincon, M. . Invited Talk (Annual Meeting do IFIP WG 1.6 Rewriting) 'Formalizing Termination in PVS'. 2021. (Apresentação de Trabalho/Conferência ou palestra).
-
De Lima, T.A. ; Ayala-Rincon, M. . Tutorial 6h Formalização de Teoremas com Assistentes de Prova - XXIX Semana do IME/UFG. 2021. (Apresentação de Trabalho/Outra).
-
De Lima, T.A. ; Ayala-Rincon, M. . Short course (8h, collocated with XII Summer Workshop on Mathematics): Interactively Proving Mathematical Theorems. 2020. (Apresentação de Trabalho/Outra).
-
Ayala-Rincon, M. . Invited Lecture on Lambda Calculus (Bernoulli Institute, Universidade de Groningen). 2020. (Apresentação de Trabalho/Outra).
-
Ayala-Rincon, M. . Invited Talk (Colloquium in Computer Science, Bernoulli Institute, U. Groningen) on Formalizing Termination. 2020. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Palestra Convidada: MAT-UFG Raciocínio Equacional Nominal Módulo. 2020. (Apresentação de Trabalho/Conferência ou palestra).
-
M. Ayala-Rincón . Invited Talk (15th LSFA) 'Nominal Equational Reasoning' 15th Logical and Semantic Frameworks with Applications. 2020. (Apresentação de Trabalho/Conferência ou palestra).
-
M. Ayala-Rincón . Invited Talk (LoReL/UBA): Termination of Functional Programs and Term Rewriting Systems. 2020. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincon, M. . Palestra (Departamento de Ciência dos Computadores, Universidade do Porto) Nominal Equational Reasoning. 2019. (Apresentação de Trabalho/Conferência ou palestra).
-
M. Ayala-Rincón . Palestra (Departamento de Ingeniería de Sistemas y Computación, Uniandes) Automation of Termination. 2019. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincon, M. . Palestra (Coloquio Departamento de Matemáticas, Universidad de Los Andes) Equational Nominal Reasoning. 2019. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincon, M. . Curso Intensivo (Universidad Nacional de Colombia - Manizales - 20h) Teoria de Prova. 2018. (Apresentação de Trabalho/Outra).
-
Ayala-Rincón, Mauricio ; Muñoz, César . Invited short course (10th International School on Rewriting ISR, Univ. Javeriana Cali - 8h): Formalization of Rewriting and Termination in a Proof Assistant. 2018. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincon, M. . Palestra (Universidad Nacional de Colombia - Manizales) Terminación de Especificaciones Funcionales. 2017. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincon, M. . Curso Intensivo (Universidad Nacional de Colombia - Manizales - 30h) Lógica Matemática. 2017. (Apresentação de Trabalho/Outra).
-
Ayala-Rincon, M. . Invited talk (WEITC, IC UFF): Treating the undecidable - the case of termination. 2017. (Apresentação de Trabalho/Congresso).
-
M. Ayala-Rincón ; Cesar Munoz ; Moscato, Mariano . Short Course (collocated with ITP/Tableaux/FroCoS): PVS for Computer Scientists. 2017. (Apresentação de Trabalho/Outra).
-
Ayala-Rincón, Mauricio . Palestra (UFG-IME) Statically Checking Termination. 2017. (Apresentação de Trabalho/Conferência ou palestra).
-
M. Ayala-Rincón . Invited talk (UNEMAT 2016): Mechanical Formalization of Computational Properties. 2016. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincon, M. . Talk (IFIP WG 1.6 Term Rewriting - Annual Meeting): Formalisation of Confluence. 2016. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Comunicação não técnica (Sem. Avaliação FAPDF-PRONEX 03/2009): Métodos Matemáticos e Computacionais. 2016. (Apresentação de Trabalho/Seminário).
-
M. Ayala-Rincón . Palestra (Universidad del Valle) Verification of Termination and Totality. 2016. (Apresentação de Trabalho/Conferência ou palestra).
-
M. Ayala-Rincón . Invited Talk (DCM 2015): Formalising Confluence. 2015. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Palestra (Escuela Colombiana de Ingeniería): Formalising Confluence. 2015. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Invited short course (Nat@Logic, 4h): Formal Reasoning with PVS. 2015. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio ; Cesar Munoz ; Moscato, Mariano ; Avelar, Andréia B . Palestra convidada (WMIMO 2015): Formalising the Automation of Termination. 2015. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincon, M. ; Cesar Munoz ; Moscato, Mariano ; Avelar, Andréia B ; Ramos, T. M. F. . Talk (King's College London): Formalising Termination. 2015. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Invited short course (8th International School on Rewriting ISR, 8h): Formalisation of Rewriting in PVS. 2014. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Invited short course (8CCC, 6h): Computational Deduction and Formal Proofs. 2013. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Invited talk (LACREST 2012): Formalising and Reusing of Proofs. 2012. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Palestra (UNQuilmes): Complexity and Algorithms for Sorting Sequences. 2012. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Palestra (UNQuilmes): Formalising and Reusing of Proofs. 2012. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Conferência convidada (IV SIMMI): Formalisation and Reusing of Proofs. 2012. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Invited talk (6CCC): Formal methods - On automating Termination. 2011. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Short course (Institut für Technik der Informationsverarbeitung/ITIV-KIT, 8h): Formal Methods Applied to the Implementation of Secure Software/Hardware using PVS. 2010. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Invited talk (ReCoSoC 2010): Automatising the verification of the termination property of algorithms and processes. 2010. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio ; Cesar Munoz ; Goodloe, Alwyn . Palestra (National Institute of Aerospace): Automating Termination in PVS by the Size-Change Principle. 2010. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio ; Cesar Munoz ; Goodloe, Alwyn . Palstra (Northeastern University): Automating Termination in PVS by Calling Context Graphs. 2010. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Conferência convidada (I SIMII): Rewriting Theory, Type Theory, Proof Theory and Verification. 2009. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Invited short course (XVII Cong. Nac. de Matemáticas, 6h): Cálculos de sustituciones explícitas con sistemas de tipos y aplicaciones en programación y demostración. 2009. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Invited talk: Rewriting, Types, Proofs and Verified Sotware and Hardware. 2009. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio ; Santos Rego, Yuri . Invited talk (II Enc. de Invest. de la Fac. de Ing. y C. Básicas, Pol. Grancolombiano): Formalisation of the Security of Cryptographic Protocols: the Dolev-Yao Model. 2009. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Invited talk (VI Encuentro Internacional de Semilleros de Investigación): Reescritura y Formalización de Software y Hardware. 2009. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Palestra (ITIV-Karlsruhe Institut für Technologie): Formal Methods, Rewriting, Proofs and Verified Software and Hardware. 2008. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Invited talk (2CCC, 2x2h): Sustituciones Explícitas en la implementación de ambientes computacionales. 2007. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Palestra (UFG): Especificação e Verificação de Sistemas Computacionais. 2007. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio ; GALDINO, André Luiz . Palestra (ULTRA, Heriot-Watt University): Verification of Rewriting Properties in PVS. 2007. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio ; SANT'ANA, Thomas Mailleux . Palestra (Escuela Colombiana de Ingeniería): SAEPTUM Verification of Rewriting Based Specifications by a Translation to Logic Theories. 2005. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio ; SANT'ANA, Thomas Mailleux . Palestra (Theorem Proving Group, Technische Universität München): SAEPTUM A Methodology for Verification of TRS via Translation to Logic Theories in PVS. 2005. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Palestra (Institut für Technik der Informationsverarbeitung, Karlsruher Institut für Technologie ITIV-KIT): Implementing String Algorithms over Reconfigurable Architectures by Rewriting-Logic. 2004. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Palestra (Université de Bretagne Occidentale): Exploring Hardware via Rewriting Logic. 2003. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio . Palestra (Institut für Technik der Informationsverarbeitung, Technische Universität Karlsruhe ITIV-TUK): On Applying ELAN Strategies in Simulating Processors over Simple Architectures. 2002. (Apresentação de Trabalho/Conferência ou palestra).
-
Ayala-Rincón, Mauricio ; KAMAREDDINE, Fairouz . Palestra (ULTRA, Heriot-Watt University): Strategies for Higher Order Unification in Explicit Substitutions. 2000. (Apresentação de Trabalho/Conferência ou palestra).
-
M. Ayala-Rincón . Resumos da Seção em Computação do II Encontro de Matemática Aplicada e Computacional em Brasília. Brasília: Departamento de Matemática, Universidade de Brasília. Apoio científico SBMAC, 2001 (Edição anais).
-
M. Ayala-Rincón . Simply Typed Calculi of Explicit Substitutions. Brasília: II Encontro de Matemática Aplicada e Computacional em Brasília. UnB/SBMAC, 2001 (Resumo estendido).
-
M. Ayala-Rincón ; Cesar Munoz . Explicit Substitutions and all that. Hanover, MD: National Aeronautics and Space Administration - NASA Centre for AeroSpace Information (CASI), 2000 (Technical Report NASA/CR-2000-210621 ICASE Report N0. 2000-45).
-
M. Ayala-Rincón ; KAMAREDDINE, Fairouz . Higher Order Unification via $\lambda s_e$-Style of Explicit Substitution. Edimburgo: Computer and Electrical Engineering, Heriot-Watt University, 1999 (Technical Report ULTRA Group Useful Logics, type Theory, Rewriting Systems and their Applications).
-
M. Ayala-Rincón . Sistemas de Reescrita de Termos. Brasília: Departamento de Matemática, Universidade de Brasília, 1996 (Mini-curso XV Jornada de Atualização em Informática - JAI96, XVI Congresso da SBC, Pernambuco).
-
M. Ayala-Rincón . Conditional Rewriting Systems with Built-in Predicates and Conjuntion of Standard Premises as Conditions. Brasília: Trabalhos de Matemática N 291, Fundação Universidade de Brasília, Departamento de Matemática, 1995 (Relatório Técnico).
Outras produções
M. Ayala-Rincón . Co-chair primeira rodada Chamada Brazil/Suiça CNPq/SNSF 29/2018. 2019.
Ayala-Rincon, M. . Membro do comitê avaliador da segunda etapa do Edital 12/2017 Startups da FAPDF. 2018.
M. Ayala-Rincón . Membro do Comitê de priorização de projetos do Edital 04/2017 ? Demanda Espontânea da FPDF. 2017.
M. Ayala-Rincón . Membro do Comitê de priorização de projetos dos Programas COFECUB e PROBRAL. 2016.
M. Ayala-Rincón . Membro do Comitê Julgador 1a rodada Edital MCT/SETEC/CNPq Nº 054/2013 ? RHAE Pesquisador na Empresa. 2014.
Ayala-Rincón, Mauricio . Membro do Comitê de Seleção de Bolsistas Doutorado e Sandúiche DAAD/CNPq-CAPES. 2014.
Ayala-Rincón, Mauricio . Membro do Comitê Julgador 2a rodada Edital MCT/SETEC/CNPq Nº 054/2013 ? RHAE Pesquisador na Empresa. 2014.
M. Ayala-Rincón . Membro do Comitê de Seleção de Bolsistas Doutorado e Sandúiche DAAD/CNPq-CAPES. 2013.
Ayala-Rincón, Mauricio . Membro do Comitê Técnico de Avaliação Propostas PAPPE Integração, Edital FAPDF 08. 2013.
Ayala-Rincon, M. . Membro do Comitê de Seleção de Bolsistas Doutorado e Sandúiche DAAD/CNPq-CAPES. 2012.
M. Ayala-Rincón . Membro do Comitê Julgador 1a rodada Edital MCT/SETEC/CNPq Nº 017/2012 ? RHAE Pesquisador na Empresa. 2012.
Ayala-Rincon, M. . Membro do Comitê Julgador 1a rodada Edital MCT/SETEC/CNPq Nº 075/2010 ? RHAE Pesquisador na Empresa. 2011.
Ayala-Rincón, Mauricio . Membro do Comitê de Seleção de Bolsistas Doutorado e Sandúiche DAAD/CNPq-CAPES. 2011.
Ayala-Rincon, M. . Membro do Comitê Julgador 2a rodada Edital MCT/SETEC/CNPq Nº 075/2010 ? RHAE Pesquisador na Empresa. 2011.
Ayala-Rincon, M. . Membro do Comitê Julgador 3a rodada Edital MCT/SETEC/CNPq Nº 075/2010 ? RHAE Pesquisador na Empresa. 2011.
Ayala-Rincon, M. . Membro do Comitê Julgador do Prêmio Pesquisador do DF. 2011.
Ayala-Rincon, M. . Membro do Comitê Julgador 1a rodada Edital MCT/SETEC/CNPq Nº 062/2009 ? RHAE Pesquisador na Empresa. 2010.
Ayala-Rincon, M. . Membro do Comitê Julgador 2a rodada Edital MCT/SETEC/CNPq Nº 062/2009 ? RHAE Pesquisador na Empresa. 2010.
Ayala-Rincon, M. . Membro do Comitê Julgador 3a rodada Edital MCT/SETEC/CNPq Nº 062/2009 ? RHAE Pesquisador na Empresa. 2010.
AYALARINCON, M . Membro do Comitê Julgador 1a Rodada do Edital MCT/SETEC/CNPq nº 67/2008 - RHAE Pesquisador na Empresa. 2009.
AYALARINCON, M . Membro do Comitê de Seleção de bolsistas DAAD/CNPq/CAPES. 2009.
Ayala-Rincón, Mauricio . Membro do Comitê Julgador 2a Rodada do Edital MCT/SETEC/CNPq nº 67/2008 - RHAE Pesquisador na Empresa. 2009.
Ayala-Rincón, Mauricio . Membro do Comitê Julgador 3a Rodada do Edital MCT/SETEC/CNPq nº 67/2008 - RHAE Pesquisador na Empresa. 2009.
Ayala-Rincón, Mauricio . Consultor ad hoc em Ciência da Computação Edital PRONEX MCT/CNPq/FAPERGS 008/2009. 2009.
AYALARINCON, M . Membro do Comitê Julgador, Edital MCT/CNPq/CT-Amazônia Nº 055/2008 - CT-Amazônia. 2008.
AYALARINCON, M . Membro do Comitê Julgador 1a Rodada do Edital MCT/SETEC/CNPq nº 32/2007 - RHAE Pesquisador na Empresa. 2008.
AYALARINCON, M . Membro do Comitê Julgador, 2a Rodada do Edital MCT/SETEC/CNPq nº 32/2007 - RHAE Pesquisador na Empresa. 2008.
AYALARINCON, M . Membro do Comitê Julgador PROBRAL (CAPES/DAAD) edital 2006. 2006.
Ayala-Rincon, M. ; Ferreira Silva, G. ; Rocha Oliveira, Ana Cristina ; Sobrinho, Daniele Nantes ; FERNANDEZ, M. ; Kutsia, T. . nominal - PVS theory for unification nominal modulo. 2024.
SERRANO, F. ; De Lima, T.A. ; M. Ayala-Rincón . Compactness Theorem for Propositional Logic and Combinatorial Applications. 2024.
De Lima, T.A. ; GALDINO, André ; Avelar, Andréia B ; Ayala-Rincon, M. . RINGS e Quaternions - parte da teoria de álgebra de PVS. 2023.
ALMEIDA, A. A. ; M. Ayala-Rincón . DEPENDENCY PAIRS - formalização em PVS da correção da automação da terminação de sistemas de reescrita por pares dependentes - Parte de NASA LaRC PVS library. 2020.
Carvalho Segundo, W.L.R. ; Rocha Oliveira, Ana Cristina ; Ferreira Silva, G. ; M. Ayala-Rincón . NOMINAL - ORTHOGONALITY - formalização em PVS da correção de mecanismos de raciocínio equacional nominal - Parte da livraria de teorias PVS de NASA LaRC. 2020.
Rocha Oliveira, Ana Cristina ; Ayala-Rincón, Mauricio . ORTHOGONALITY - formalização em PVS do teorema de confluência de sistemas de rescrita ortogonais - Parte de NASA LaRC PVS library. 2013.
Santos Rego, Yuri ; NOGUEIRA, R. B. ; M. Ayala-Rincón . Formalização da segurança do modelo criptográfico de Dolev Yao em PVS. 2012.
Avelar, Andréia B ; GALDINO, André Luiz ; Ayala-Rincon, M. . UNIFICATION, uma teoria PVS para unificação em sistemas de primeira ordem - Parte de NASA LaRC PVS library. 2011.
Ayala-Rincon, M. ; Cesar Munoz ; Goodloe, Alwyn . Terminação pelo "size-change principle" via grafos de contextos de chamados em PVS. 2010.
ARBOLEDA, Daniel Muñoz ; LLANOS, Carlos ; M. Ayala-Rincón ; van ELS, R. . Sistema de Controle Distribuído de Grupo de Elevadores Usando Dispositivos Reconfiguráveis. 2009.
GALDINO, André Luiz ; AYALARINCON, M . TRS - PVS theory for term rewriting systems - Parte de NASA LaRC PVS library. 2008.
GALDINO, André Luiz ; AYALARINCON, M . ARS - PVS theory for abstract reduction systems - Parte de NASA LaRC PVS library. 2007.
SANT'ANA, Thomas Mailleux ; M. Ayala-Rincón . SAEPTUM uma ferramenta de translação de especificações de reescrita em ELAN para teorias lógicas. 2005.
MORRA, Carlos ; BECKER, Jürgen ; M. Ayala-Rincón ; HARTENSTEIN, Reiner W . FELIX: utilização de reescrita-lógica para geraçao de implementações funcionalmente equivalentes. 2005.
MOURA, Flávio Leonardo Cavalcanti de ; M. Ayala-Rincón . SUBSEXPL uma ferramenta para comparação de cálculos de substituições explícitas. 2004.
M. Ayala-Rincón ; SILVA, A. H. R. ; FONSECA, A. F. ; NOGUEIRA, R. B. . Sistema de Animação Gráfica para Visualização de Relações de Equivalência entre Modelos e Representações Gramaticais de Linguagens Formais - SAGEMoLiC. 2001.
M. Ayala-Rincón ; SILVA, A. H. R. . Sistema de Animação Gráfica de Algoritmos para Reconhecimento de Padrões em Palavras - SAGAReP. 1999.
M. Ayala-Rincón ; L. M. R. Gadelha . Algoritmo de decisão para a aritmética de Presburger. 1995.
Ayala-Rincon, M. ; Mimram, S. . Proceedings of the 9th International Workshop on Confluence IWC 2020 (with system descriptions from CoCo 2020). 2020. (Editoração/Anais).
Ayala-Rincon, M. ; Balbiani, Philippe . Special Issue on Unification in Mathematical Structures in Computer Sciences. 2020. (Editoração/Periódico).
Projetos de pesquisa
-
2025 - Atual
Coordenador em Brasil Projeto de Cooperação IES\R3\243187 "Formal Verification of Practical Nominal Unification Algorithms", Descrição: Coordenador na Grã Bretanha: Mohammad Abdulaziz - Coordenador em Brasil: Mauricio Ayala-RinconErros de software podem ter consequências financeiras e sociais sérias (por exemplo, o escândalo dos Correios em U.K.). Para evitá-los, a maioria dos desenvolvedores usa testes, que identificam casos em que o programa não está em conformidade com as propriedades desejadas, mas não podem descartar completamente a presença de bugs. No entanto, aplicativos em domínios críticos de segurança (por exemplo, sistemas autônomos e de saúde) exigem provas formais de correção do software usado, ou seja, garantias matemáticas de que um programa está em conformidade com as propriedades desejáveis. Essas provas podem ser construídas de forma viável usando provadores de teoremas (por exemplo, Coq, Lean, Isabelle/HOL, PVS). Os provadores de teoremas foram realmente usados #8203;#8203;com sucesso para provar a correção de muitos sistemas impressionantes, como kernels de sistemas operacionais e compiladores.No entanto, os provadores de teoremas interativos modernos são, eles próprios, peças complicadas de software, cuja confiabilidade depende da correção de muitos de seus componentes confiáveis, ou seja, componentes que não são verificados e cuja saída é considerada pelo valor de face. Um dos componentes mais importantes na maioria dos provadores de teoremas são os algoritmos de unificação. Algoritmos de unificação são uma noção-chave em álgebra, bem como um bloco de construção-chave em linguagens de programação declarativas, além de provadores de teoremas.Neste projeto, trabalharemos para verificar formalmente um algoritmo de unificação prático, que será usado em dois provadores de teoremas populares: Isabelle/HOL e PVS. Isso aumentará significativamente a confiabilidade desses dois provadores de teoremas, o que, por sua vez, aumentará a confiabilidade do software que é verificado usando esses dois sistemas.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Mauricio Ayala Rincon - Coordenador / Daniele Nantes Sobrinho - Integrante / Thaynara Arielly de Lima - Integrante / Maribel Fernández - Integrante / Christian Urban - Integrante / David Wang - Integrante / Marcus Mercandeli - Integrante / Guilherme Borges Brandão - Integrante / Mohammad Abdulaziz - Integrante., Financiador(es): Royal Society - Cooperação.
-
2023 - Atual
FAPEG 202310267000223 (CAP2022061000121 Ed. 03/2022) - Formalização de Estruturas Algébricas e Computacionais, Projeto certificado pelo(a) coordenador(a) Thaynara Arielly de Lima em 19/06/2023., Descrição: Elaboração de arcabouços formais acerca de teorias algébricas no sistema PVS, especificamente, sobre os anéis dos polinômios e dos Quaternions, além de aplicações, com o intuito de prover suporte ao desenvolvimento formal de sistemas computacionais, algoritmos e teorias, que possuam tais objetos em seu escopo.. , Situação: Em andamento; Natureza: Pesquisa. , Integrantes: Mauricio Ayala Rincon - Integrante / André Galdino - Integrante / Andréia Borges Avelar - Integrante / Thaynara Arielly de Lima - Coordenador.
-
2022 - 2024
Coordenador do projeto Demanda Espontânea (FAPDF DE 00193.00001175/2021-11), Descrição: O projeto inclui um time de pesquisadores dos Institutos de Ciências Exatas da UnB e da UFG, assim como da UFCat e da UnB sede Planaltina. O objetivo é desenvolvimento de técnicas nominais para raciocínio equacional computacional, e a formalização no assistente de demonstração PVS de teoremas relacionados com automação da terminação de programas funcionais, assim como a formalização de teoremas algébricos para anéis não comutativos e suas aplicações.O projeto envolve cooperação com pesquisadores de AMA/NASA LaRC, King's College London, Johannes Kepler University Linz, através de implementação de visitas à UnB e co-orientações de mestrado e doutorado.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Mestrado acadêmico: (1) Doutorado: (6) . , Integrantes: Mauricio Ayala Rincon - Coordenador / Flávio Leonardo Cavalcanti de Moura - Integrante / Daniel Lima Ventura - Integrante / André Luiz Galdino - Integrante / Andréia Borges Avelar - Integrante / Daniele Nantes Sobrinho - Integrante / Thaynara Arielly de Lima - Integrante / Thiago Mendoça Ferreira Ramos - Integrante / Gabriel Ferreira Silva - Integrante / Mehwish Arshid - Integrante / Andrés Felipe González Barragán - Integrante / Ali Khãn Caires Ribeiro Santos - Integrante / Leonardo Melo Batista - Integrante.
-
2022 - Atual
Coordenador do projeto Universal CNPq (processo 409003/2021-2) Terminação e Estruturas Algébricas em Computação, Descrição: O objetivo principal é a exploração da aplicabilidade de diversos arcabouços formais, como a teoria de reescrita, a teoria de tipos, a teoria de prova e as estruturas algébricas, no desenvolvimento de sistemas computacionais e dedutivos e na implementação de soluções algorítmicas provadas corretas e eficientes.Sem negligenciar as aplicações, um elemento central de análise é otratamento de mecanismos dedutivos equacionais e algébricos para sistemas de raciocínio computacional via formalização de estruturas algébricas e suas propriedades, além da aplicação de técnicas das áreas de lógica, sintaxe e semântica nominal. Com esses arcabouços formais, a pesquisa realizada aproxima a teoria da prática computacional, sendo assim de grande importância e atualidade para fornecer novas técnicas para a implementação e desenho de ferramentas inovadoras de especificação (linguagens de programação e de computação simbólica, que permitem, por exemplo, implementar métodos de computação numérica) e dedução (associadas à automação do raciocínio e de processos de inferência via assistentes de provas, cerne de aplicações em Inteligência Artificial via programação lógica) que dão suporte ao desenvolvimento formal de sistemas computacionais robustos e matematicamente provados corretos.O projeto envolve cooperação com pesquisadores de AMA/NASA LaRC, King's College London, Johannes Kepler University Linz, através de implementação de visitas à UnB e co-orientações de mestrado e doutorado.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Mestrado acadêmico: (1) Doutorado: (6) . , Integrantes: Mauricio Ayala Rincon - Coordenador / Flávio Leonardo Cavalcanti de Moura - Integrante / André Luiz Galdino - Integrante / Cláudia Nalon - Integrante / Andréia Borges Avelar - Integrante / Daniele Nantes Sobrinho - Integrante / Thaynara Arielly de Lima - Integrante / Thiago Mendoça Ferreira Ramos - Integrante / Gabriel Ferreira Silva - Integrante / Almeida, Ariane A. - Integrante / Mehwish Arshid - Integrante / Andrés Felipe González Barragán - Integrante / Ali Khãn Caires Ribeiro Santos - Integrante / Nikson Bernardes Fernandes Ferreira - Integrante.
-
2019 - 2024
Coordenador do projeto CAPES PrInt MAT-UnB entre 2019-22 - Desde 2022, em andamento sob coordenação do PPG MAT UnB, Descrição: Projeto PrInt do PPG em Matemática da UnB envolvendo pesquiadores e aluno do PPG em Matemática da UnB em áreas como análise, geometria, probabilidade, sistemas dinâmicos, mecânica, e teoria da computação. Especificamente, na última área, inclui cooperação efetiva com o Pesquisador Jorge A. Pérez do Bernoulli Institute for Mathematics and Artificial Intelligence da Groningen University. Adicionalmente, o projeto inclui cooperação com o pesquisador Temur Kutsia do RISC Johannes Kepler University Linz, através de visitas de cooperação à UnB e co-supervisão de alunos de doutorado.. , Situação: Concluído; Natureza: Pesquisa. , Integrantes: Mauricio Ayala Rincon - Coordenador / Vander Ramos Alves - Integrante / Daniele Nantes Sobrinho - Integrante / Keti Tenenblat - Integrante / Marcelo F. Furtado - Integrante / Carlos Alberto P. dos Santos - Integrante / Yuri Dumaresq Sobral - Integrante / Pedro Roitman - Integrante / Leandro Martins Cioletti - Integrante / Mauro Padrão - Integrante / Giovani de Jesus Malcher Figueiredo - Integrante / Jiazheng Zhou - Integrante / Liliane de Almeida Maia - Integrante / Luis Henrique de Miranda - Integrante / Miguel Ângelo Marini - Integrante / Ricardo Bomfim Machado - Integrante / Rosana Tidon - Integrante / Ludmilla Moura de Souza Aguiar - Integrante / William Cintra da Silva - Integrante / João Paulo dos Santos - Integrante / Camilo Chang Dórea - Integrante / Mercedes Maria da Cunha Bustamante - Integrante / Lucas Conque Seco Ferreira - Integrante / Mauro Morais Alves Padrão - Integrante / Ricardo Silva Azevedo Araújo - Integrante / Paulo Henrique Pereira da Costa - Integrante / Eduardo Antônio da Silva - Integrante / Jorge Pérez - Integrante / Alen Arslanagic - Integrante / Joseph Paulus - Integrante / Antonio Suárez Fernández - Integrante / Blanca Climent Ezguerra - Integrante / Cristian Morales Rodrigo - Integrante / Francisco Guillén Gonzáles - Integrante / María Ángeles Rodríguez Bellido - Integrante / David Arcoya - Integrante / David Ruiz - Integrante / Angela Pistoia - Integrante / Eugenio Montefusco - Integrante / Filomena Pacella - Integrante / Lucio Boccardo - Integrante / Luca Fanelli - Integrante / Luigi Orsina - Integrante / Massimo Grossi - Integrante / Minbo Yang - Integrante / Zhigui Lin - Integrante / Antonio Martinez - Integrante / Huai-Dong Cao - Integrante / Martin Rasmussen - Integrante / Adrián Andrada - Integrante / Jorge Lauret - Integrante / Andrew Trigg - Integrante / Nicolas Taberlet - Integrante., Financiador(es): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - Auxílio financeiro.
-
2019 - 2024
CAPES PrInt PPG Informática UnB, Descrição: Projeto CAPES PrInt do PPG em Informática da Universidade de Brasília. Neste projeto, coordeno a cooperação em técnicas de automação da terminação com participação do pesquisador Mariano Miguel Moscato (AMA/NASA LaRC Formal Methods), e em compressão gramatical com Gonzalo Navarro (Universidade de Chile), com participação de alunos de mestrado e doutorado do PPG em Informática da UnB. O projeto inclui co-supervisão destes dois pesquisadores de alunos de doutorado e mestrado, assim como implementação de visitas à UnB.. , Situação: Concluído; Natureza: Pesquisa. , Integrantes: Mauricio Ayala Rincon - Integrante / Alba Cristina Magalhaes Alves de Melo - Integrante / Maria Emilia Machado Telles Walter - Integrante / Cláudia Nalon - Integrante / Daniel Saad Nogueira Nunes - Integrante / André Costa Drummond - Integrante / Mariano Moscato - Integrante / Thiago Mendoça Ferreira Ramos - Integrante / Gonzalo Navarro - Integrante / Gabriel Ferreira Silva - Integrante / Bruno Luiggi Macchiavello Espinoza - Coordenador / Teofilo Emidio de Campos - Integrante.
-
2019 - 2022
Participação em projeto (FAPDF DE ), Projeto certificado pelo(a) coordenador(a) Andréia Borges Avelar em 25/02/2023., Descrição: Formalização no assistente PVS da teoria de anéis. Projeto com participação de pesquisadores da UnB, UFG, UFCat, e UnB sede Planaltina.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (1) . , Integrantes: Mauricio Ayala Rincon - Integrante / André Luiz Galdino - Integrante / Andréia Borges Avelar - Coordenador / Ana Cristina Rocha Oliveira - Integrante / Thaynara Arielly de Lima - Integrante / André Camapum Carvalho de Freitas - Integrante.
-
2017 - 2020
Coordenador Projeto Demanda Espontânea (FAPDF 193.001.369/2016) Estruturas Formais para Computação e Dedução, Descrição: O objetivo geral da pesquisa é a exploração da aplicabilidade da teoria de reescrita, dos cálculos de substituições explícitas, da sintaxe e lógica nominal, da teoria de tipos e da teoria de prova no desenvolvimento de sistemas computacionais e na implementação de soluções algorítmicas corretas e eficientes aplicadas em diversas áreas e em particular em mecanismos de dedução equacional (casamento, unificação e estreitamento) com aplicações de destaque como raciocínio de segurança e integridade de sistemas de comunicação e protocolos criptográficos. O projeto incluiu atividades de cooperação, visitas técnicas à UnB e missões de trabalhao, com pesquisadores do National Institute of Aerospace, Heriot-Watt University, King´s College London.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (2) / Doutorado: (4) . , Integrantes: Mauricio Ayala Rincon - Coordenador / Flávio Leonardo Cavalcanti de Moura - Integrante / Daniel Lima Ventura - Integrante / André Luiz Galdino - Integrante / Andréia Borges Avelar - Integrante / Maribel Fernández - Integrante / Daniel Saad Nogueira Nunes - Integrante / NANTES-SOBRINHO, DANIELE - Integrante / Ariane Alves Almeida - Integrante / Lucas Angelo da Silveira - Integrante / Thiago Mendoça Ferreira Ramos - Integrante / ROCHA-OLIVEIRA, ANA CRISTINA - Integrante / Cesar Muñoz - Integrante / Fairouz Kamareddine - Integrante / Mariano Moscato - Integrante., Financiador(es): Fundação de Apoio à Pesquisa do Distrito Federal - Auxílio financeiro.
-
2014 - 2015
Coordenador Técnico de Projeto Cooperação Internacional CsF/BJT (processo 401319/2014-8 do Programa Ciência sem Fronteiras CNPq), Reescrita com Cobertura de Ordem Superior, Descrição: BJT Besik Dundua. Many programming languages contain higher-order functions. For declarative programming, higher-order features are very useful for applications that involve variable binding. Growing importance of rule-based technologies for academia and industry, applications such as Web, processing human language, data, legal norms, etc. justify interest to rule-based formalisms and tools. We believe that higher-order rule-based programming with hedge variables will be an important contribution in the development of such rule technologies. Its foundational formalism, higher-order rewriting with hedge variables, is the topic of this proposal.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Doutorado: (1) . , Integrantes: Mauricio Ayala Rincon - Coordenador / Flávio Leonardo Cavalcanti de Moura - Integrante / Daniele Nantes Sobrinho - Integrante / Besik Dundua - Integrante / Temur Kutsia - Integrante.
-
2013 - 2017
Coordenador de Projeto UNIVERSAL 476952/2013-1 Formalização de Sistemas Computacionais com Substituições Explícitas, Terminação e Aplicações, Descrição: O objetivo geral da nossa pesquisa é a exploração da aplicabilidade da teoria de reescrita, dos cálculos de substituições explícitas, da teoria de tipos e da teoria de prova no desenvolvimento de sistemas computacionais e na implementação de soluções algorítmicas corretas e eficientes aplicadas a diversas áreas. A teoria de reescrita é um mecanismo efetivo e bem estabelecido de programação com aplicações em diversas áreas. Com efeito, diversos ambientes de programação e dedução como Maude dependem de um formalismo teórico baseado diretamente em sistemas de reescrita de ordem superior com suporte de sistemas de tipos elaborados. Ambientes de especificação bem conhecidos utilizam mecanismos essenciais da teoria de reescrita como {\em matching}, simplificação e unificação (c.f. Isabelle/HOL, Coq, $\lambda$Prolog, PVS, etc). O GTC/UnB tem desenvolvido aplicações da teoria de reescrita em contextos que vão da modelagem de {\em hardware} eficiente até a verificação de {\em software} crítico. É neste contexto que a presente proposta está focada; mais especificamente, na formalização de propriedades de cálculos de substituições explícitas e na automatização da propriedade de terminação de processos computacionais.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (2) / Doutorado: (4) . , Integrantes: Mauricio Ayala Rincon - Coordenador / Flávio Leonardo Cavalcanti de Moura - Integrante / Daniel Lima Ventura - Integrante / André Luiz Galdino - Integrante / Andréia Borges Avelar - Integrante / Daniele Nantes Sobrinho - Integrante / Ana Cristina Rocha Oliveira - Integrante / José Luis Soncco-Álvarez - Integrante / Thaynara Arielly de Lima - Integrante / Daniel Saad Nogueira Nunes - Integrante., Número de produções C, T & A: 9
-
2013 - 2015
Coordenador Técnico de Projeto Cooperação Internacional CsF/PVE (0500/2013, processo 23038.009845-2012/81, 146/2012 do Programa Ciência sem Fronteiras CAPES-CNPq), Ferramentas para a análise de Sistemas de Reescrita Nominais, Descrição: Nominal sets provide a new mathematical basis for the analysis of names and binding. Nominal rewriting systems are used to specify the dynamics of systems with binding operators such as specification and programming languages, computation models and, in general, formal models for the development of certified and secure computational systems. This project will investigate whether well known tools, such as type systems, can be used to provide semantics and analyse termination properties of nominal rewriting systems. Nominal rewriting is an important alternative as a formalism to define explicit substitutions calculi, field in which the Brazilian team has obtained a recognised record of results. This cooperation will bring together the expertise in nominal rewriting and type systems of the group headed by Prof. Maribel Fernández (who is the PVE of this project) and the knowledge in explicit substitutions calculi enlarged with type systems of the Brazilian team in order to build elaborated type systems for nominal rewriting and related applications in formal methods and security.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Mauricio Ayala Rincon - Coordenador / Daniele Nantes Sobrinho - Integrante / Ana Cristina Rocha Oliveira - Integrante / Maribel Fernández - Integrante / Washington Luis Ribeiro de Carvalho Segundo - Integrante., Financiador(es): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - Auxílio financeiro.
-
2012 - 2014
Coordenador do projeto de cooperação internacional STIC-AmSud Brasil/França/Argentina (130/2011 CAPES/INRIA/MINCYT), Desenvolvimento Formal de Programas e Aplicações - DeCoPA, Descrição: Universidade de Brasília, Université Paris 7, Universidad de Quilmes. Coordenação Argentina: Eduardo Bonelli, Coordenação França: Antonio Bucciarelli e Delia Kesener, Coordenação Brasileira: Flávio L.C. de Moura, Coordenação geral: Mauricio Ayala Rincon.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (1) / Doutorado: (3) . , Integrantes: Mauricio Ayala Rincon - Coordenador / Edward Hermann Haeusler - Integrante / André Galdino - Integrante / Daniel Lima Ventura - Integrante / Delia Kesner - Integrante / Alejandro Ríos - Integrante / Elaine Pimentel - Integrante / Andréia Borges Avelar - Integrante / Daniele Nantes Sobrinho - Integrante / de Moura, F.L.C. - Integrante / Ana Cristina Rocha Oliveira - Integrante / Eduardo Bonelli - Integrante / Antonio Bucciarelli - Integrante., Financiador(es): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - Auxílio financeiro.
-
2010 - 2015
Coordenador do projeto PRONEX 2009/00091-0 (193.000.580/2009), Métodos Matemáticos e Computacionais: Teoria e Aplicações em Modelagem de Processos Biomecânicos, Algorítmicos e Estocásticos, Descrição: Projeto PRONEX em matemática pura e aplicada, que envolve mais de 20 pesquisadores de produtividade do CNPq dos Programas de Pós-graduação em Matemática e Informática da UnB. No período de execução do projeto o grupo orientou mais de 50 e 80 teses e dissertações e publicou mais de duas centenas de artigos.. , Situação: Concluído; Natureza: Pesquisa. , Integrantes: Mauricio Ayala Rincon - Coordenador / Flávio Leonardo Cavalcanti de Moura - Integrante / Noraí Romeu Rocco - Integrante / Pavel Shumyatsky - Integrante / Alba Cristina Magalhaes Alves de Melo - Integrante / Alexei Krassalnikov - Integrante / Pavel Zalesski - Integrante / Said Sidki - Integrante / Aline Gomes da Silva Pinto - Integrante / Hemar Teixeira Godinho - Integrante / Jorge Carlos Lucero - Integrante / Keti Tenenblat - Integrante / Chang Chung Yu Dorea - Integrante / Wang Qiaoling - Integrante / Xia Changyu - Integrante / Elves A. de Barros e Silva - Integrante / Marcelo F. Furtado - Integrante / Irina Sviridova - Integrante / Carlos Alberto P. dos Santos - Integrante / Yuri Dumaresq Sobral - Integrante / Pedro Roitman - Integrante / Ary Vasconcelos Medino - Integrante / Cátia Regina Gonçalves - Integrante / Leandro Martins Cioletti - Integrante / Mauro Rabelo - Integrante / Daniele S. B. Martins Neto - Integrante / Kellcio Oliveira Araújo - Integrante / Luciana de A. Rodrigues - Integrante / Carlos M. C. Riveros - Integrante / Sheila Campos Chagas - Integrante / José Antônio O. de Freitas - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro / Fundação de Apoio à Pesquisa do Distrito Federal - Auxílio financeiro.
-
2010 - 2012
Coordenador do projeto UNIVERSAL 481783/2010-5: Substituições Explícitas, Terminação, Formalização de Sistemas e Aplicações Computacionais, Descrição: Dois são os objetos centrais da pesquisa proposta: implementação explícita da substituição e automatização da propriedade de terminação. A primeira, uma operação básica em ambientes de programação e dedução computacionais e a segunda, uma propriedade bem conhecida indecidível, mas com critérios de terminação bem estudados por décadas, de forma que permite a sua automação em linguagens de programação e assistentes de prova. O objetivo quanto aos cálculos de substituições explícitas não se limita à formalização utilizando apenas papel e lápis, mas engloba a especificação e verificação formal de propriedades computacionais relevantes destes cálculos em assistentes de prova como o Coq, PVS e Isabelle/HOL. Quanto à automação da terminação pretende-se construir uma "teoria" (livraria) na linguagem do assistente de prova PVS para o tratamento da propriedade de terminação. Essa "teoria" incluirá critérios matemáticos para verificação de terminação de sistemas especificados via regras de reescrita de termos e desenvolverá estratégias de redução-módulo teorias entre as quais destacamos teorias equacionais associativas comutativas. Mecanismos para o tratamento da dedução módulo esse tipo de teorias equacionais são relevantes para o manuseio algébrico eficiente de especificações em geral. A base para essa teoria será a metodologia de grafos de contextos de dependência desenvolvida por Manolios e implementada com sucesso no assistente de demonstração ACL2.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Doutorado: (2) . , Integrantes: Mauricio Ayala Rincon - Coordenador / Flávio Leonardo Cavalcanti de Moura - Integrante / Daniel Lima Ventura - Integrante / Cláudia Nalon - Integrante / Andréia Borges Avelar - Integrante / Daniele Nantes Sobrinho - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro., Número de produções C, T & A: 1
-
2008 - 2010
Coordenador do projeto FAPDF 8-004/2007, Verificação Formal de Protocolos de Comunicação com Aplicações em Criptografia, Descrição: Abordam-se sistemas computacionais corretos e seguros que especificam propriedades fundamentais de protocolos criptográficos via o assistente de prova PVS.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (2) . , Integrantes: Mauricio Ayala Rincon - Coordenador / Flávio Leonardo Cavalcanti de Moura - Integrante / Alba Cristina Magalhaes Alves de Melo - Integrante / Cláudia Nalon - Integrante / Guilherme Albuquerque Pinto - Integrante., Financiador(es): Fundação de Apoio à Pesquisa do Distrito Federal - Auxílio financeiro., Número de produções C, T & A: 2
-
2008 - 2010
Coordenador brasileiro do projeto CNPq/DFG 490396/2007-0 Concepção de aplicações em bioinformática e outras áreas sobre sistemas reconfiguráveis com baixo consumo de potência, Descrição: Cooperação Brasil/Alemanha entre os Departamentos de Matemática, Computação e Mecatrônica da Universidad de Brasília e o Institut für Technik der Informationsverarbeitung (ITIV) da Universität Karlsruhe. Pesquisadores envolvidos: Reiner Hartenstein, Jüegen Becker (coordenador alemão), Carlos Morra, Michael Hübner, Ricardo P. Jacobi, Carlos Llanos, Alba C.M.A. de Melo, Maria Emilia Telles Walter, Flávio L.C. de Moura.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (2) / Doutorado: (2) . , Integrantes: Mauricio Ayala Rincon - Integrante / Jürgen Becker - Coordenador., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro., Número de produções C, T & A: 1
-
2008 - 2009
Participação em Projeto PROBRAL (CAPES/DAAD), Processo 304/08, Formally Designed Reconfigurable Architectures for High Performance Applications, Descrição: Projeto de cooperação entre as Universidadaes de Brasília, Universidade Federal de Rio Grande do Sul e a Universität Karlsruhe. Coordenador Brasileiro Ricardo P. Jacobi; Coordenador Alemão Jürgen Becker.. , Situação: Em andamento; Natureza: Pesquisa. , Integrantes: Mauricio Ayala Rincon - Coordenador / Reiner W Hartenstein - Integrante / Ricardo P Jacobi - Integrante / Carlos Llanos - Integrante / Jürgen Becker - Integrante / Ricardo A L Reis - Integrante / Sergio Bampi - Integrante.
-
2005 - 2007
Coordenador do projeto UNIVERSAL 471791/2004-0: Teoria Semântica, Lógica e Aplicações da Computação, Descrição: Cálculos de substituições explícitas são sistemas de reescrita de ordem superior ou variações do lambda cálculo, onde a operação de substituição é definida explicitamente. Estes cálculos ficam muito próximos das implementações de sistemas que suportam representações de ordem superior de objetos como programas e provas. As propriedades desejáveis dos cálculos de substituições explícitas estão relacionadas com a simulação do próprio lambda cálculo e com aquelas dos sistemas de reescrita e estão ligadas a conceitos computacionais como o determinismo ou unicidade das respostas (confluência), efetividade dos processos algorítmicos (terminação), etc. Mas até o momento não se tem desenvolvido um cálculo de substituições explícitas completamente satisfatório: tais propriedades estão interligadas e ao ser forçada a satisfação de alguma, outra(s) deixa(m) de valer. O objetivo principal deste projeto é a exploração da aplicabilidade dos destes cálculos na implementação de assistentes de prova e de linguagens de programação. Serão desenvolvidos mecanismos para abordar eficientemente problemas como a unificação de ordem superior, baseados em métodos formulados sobre os cálculos de substituições explícitas. Para isto comparam-se diversos cálculos de substituições explícitas determinando quais são mais adequados para cada problema. Os principais problemas a serem analisados são aqueles relacionados com unificação de ordem superior, com ênfase nos redutos onde se tem decidibilidade. A saber, os padrões de ordem superior e matching de ordens 2, 3 e 4. Adicionalmente, é nosso intuito aprimorar os mecanismos existentes em um provador de teoremas para lógicas cujos modelos são domínios não-decrescentes. Embora existam vários provadores para lógicas de ordem superior, há um crescente interesse em provadores específicos para lógicas modais, tais como as temporais e epistêmicas, já que estas linguagens expressam, de modo natural, problemas computacionais complexos.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Especialização: (0) / Mestrado acadêmico: (2) / Mestrado profissional: (0) / Doutorado: (2) . , Integrantes: Mauricio Ayala Rincon - Coordenador / Flávio Leonardo Cavalcanti de Moura - Integrante / Hélio Carneiro Ferreira - Integrante / Alba Cristina Magalhaes Alves de Melo - Integrante / Daniel Lima Ventura - Integrante / Aline Cosme da Cunha - Integrante / André Luiz Galdino - Integrante / Cláudia Nalon - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro., Número de produções C, T & A: 2
-
2005 - 2007
Coordenador do projeto CT-INFO 506598/04-7: Simulação Algorítmica, Semântica e Aplicações da Computação, Descrição: Desenvolvimento de aplicativos para simulação algorítmica da produção de fala e semântica e aplicações da computação. Para o último desenvolvem-se extensões do sistema SUBSEXLP nas quais combinações da beta-contração são admitidas. Além de alunos estão envolvidos os Professores Jorge C. Lucero (a cargo do primeiro item) e Cláudia Nalon.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Especialização: (0) / Mestrado acadêmico: (2) / Mestrado profissional: (0) / Doutorado: (1) . , Integrantes: Mauricio Ayala Rincon - Coordenador / Flávio Leonardo Cavalcanti de Moura - Integrante / Hélio Carneiro Ferreira - Integrante / André Galdino - Integrante / Daniel Lima Ventura - Integrante / Aline Cosme da Cunha - Integrante / Cláudia Nalon - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro., Número de produções C, T & A: 4
-
2001 - 2011
Participação em projetos conjuntos com o grupo ULTRA, Heriot-Watt University, Edimburgo (Escócia): Unificação de Ordem Superior Simples Tipada via Cálculos de Substituições Explícitas. Recursos de programas Auxílio Complementar à Pesquisa DPP/UnB e E, Descrição: Estudo de aplicabilidade dos cálculos de substituições explícitas na unificação de ordem superior tratada como operação necessária em ambientes computacionais de ordem superior. Estudo de sistemas de tipos elaborados em cálculos de substituições explícitas. Recursos utilizados incluem: auxílio de Projeto Universal CNPq (2002-2003), bolsas de pesquisa CNPq (2003-2007 e 2007-2010), Bolsa CAPES de Doutorado Sanduiche (2004-2005), Bolsa CNPq de Doutorado Sanduiche (2007-2008), Bolsas PIBIC/CNPq (2003-2004, 2004-2005,2004-2007,2007-2010). Recursos de participação em projeto "Métodos Determinísticos e Não Determinísticos" Programa de Apoio à Núcleos de Excelência - PRONEX, Edital 001/2003 - Convênio 0096-00/2004 SDCT/FAPDF/MCT/CNPq.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (4) / Especialização: (0) / Mestrado acadêmico: (3) / Mestrado profissional: (0) / Doutorado: (2) . , Integrantes: Mauricio Ayala Rincon - Coordenador / Fairouz Kamareddine - Integrante / Flávio Leonardo Cavalcanti de Moura - Integrante / Hélio Carneiro Ferreira - Integrante / Marrise Neves da Rocha - Integrante / Daniel Lima Ventura - Integrante / Aline Cosme da Cunha - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro / Conselho Nacional de Desenvolvimento Científico e Tecnológico - Bolsa / Conselho Nacional de Desenvolvimento Científico e Tecnológico - Bolsa / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - Bolsa / Conselho Nacional de Desenvolvimento Científico e Tecnológico - Bolsa., Número de produções C, T & A: 20
-
2001 - 2003
Coordenador do projeto UNIVERSAL 47488/01-6 Teoria e Semântica da Computação., Descrição: Pesquisa em aplicações dos cálculos de substituições explícitas e sistemas de reescrita em métodos formais.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (2) . , Integrantes: Mauricio Ayala Rincon - Coordenador / Fairouz Kamareddine - Integrante / Cesar Augusto Hurtado Munoz - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.
-
1997 - 1998
Coordenador projeto FAPDF 193033/96 Combinação de Predicados Pré-construídos e de Especificações Equacionais com Técnicas de Reescrita., Descrição: Combinação de Predicados Pré-construídos e de Especificações Equacionais com Técnicas de Reescrita. Com Auxílio adicional do programa SOS-pesquisa DPP/UnB.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (2) . , Integrantes: Mauricio Ayala Rincon - Coordenador / Haydée Werneck Poubel - Integrante., Financiador(es): Fundação de Apoio à Pesquisa do Distrito Federal - Auxílio financeiro.
-
1995 - 1997
Participação em projeto FAPDF 193363/95 Métodos Computacionais e Otimização, Descrição: Coordenação das atividades relacionadas com instalações e aplicações computacionais em aplicações da teoria de reescrita.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (1) . , Integrantes: Mauricio Ayala Rincon - Integrante / Haydée Werneck Poubel - Integrante / Maria Helena Cautiero Horta Jardim - Coordenador., Financiador(es): Fundação de Apoio à Pesquisa do Distrito Federal - Auxílio financeiro.
-
1995 - 1996
Coordenador projeto FAPDF 193099/95 Atualização da Capacidade Computacional do Laboratório de Cálculo, Descrição: Atualização da Capacidade Computacional do Laboratório de Cálculo do PPG em Matemática da UnB.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) . , Integrantes: Mauricio Ayala Rincon - Coordenador / Haydée Werneck Poubel - Integrante., Financiador(es): Fundação de Apoio à Pesquisa do Distrito Federal - Auxílio financeiro.
Prêmios
2025
"Honorable Mention" awarded to the paper "Verification of an Anti-Unification Algorithm in PVS", NASA Formal Methods Symposium - Program Chairs.
2023
"Best Paper Award" - "Nominal AC-Matching", Int. Conference on Intelligent Computational Mathematics, CICM 2023, Cambridge.
2021
Eleito Membro titular, IFIP WG 1.6: Rewriting.
2020
Eleito membro do Steering Committee da International Conference on Interactive Theorem Proving ITP, International Conference on Interactive Theorem Proving.
2018
Eleito membro do Steering Committee da International Conference on Formal Structures for Computation and Deduction FSCD, IFIP Working Group 1.6 on Rewriting e General Assembly de FSCD 2018 em Oxford.
2013
Melhores Trabalhos em TC CLEI 2013 - convite publicação em special issue Elsevier ENTCS, CLEI.
2012
Eleito membro do Steering Committee da International Conference on Rewriting Techniques and Applications, IFIP Working Group 1.6 on Rewriting e General Assembly da conferência RTA em Nagoya.
2012
Aprovado em 1o lugar em concurso público para Professor Titular em Matemática, Dep. de Matemática, UnB (Banca: K Tenenblat, CL Lucchesi, C Tomei, JA Cuminato, FCP Milies).
2012
Orientador do melhor projeto em seção da área de Computação. Aluna Jéssyca Cristine Lima de Souza, Programa de Iniciação Científic DPP/Universidade de Brasília.
2012
Melhores Trabalhos em TC CLEI 2012 - convite publicação em special issue Elsevier ENTCS, CLEI.
2009
Nomeado "Professor" da Universidad Autónoma de Bucaramanga UNAB, Reitoria da UNAB (Reitor: Alberto Montoya Puyana) e SCC (Presidente: Eduardo Carrillo Zambrano).
2009
Prêmio Pesquisador do Distrito Federal, classificado em segundo lugar na Categoria Exatas e da Terra, Fundação de Apoio à Pesquisa do Distrito Federal FAPDF.
2009
Orientador do melhor projeto de Iniciação Científica da área - Sessão Matemática, Aluna Ana Cristina Rocha Oliveira, Programa de Iniciação Científica DPP/UnB..
2009
Aprovado em primeiro lugar em concurso público para Professor Titular em computação, Dep. Ciência da Computação UnB (Banca: NR Rocco, LFG Soares, T Kowaltowski, CL Luccesi).
2007
Melhores Trabalhos CLEI 2007 - convite publicação número especial CLEI Elec. Journal, CLEI.
2006
Synplicity award for best latin-american R&D group on ReConFigurable Computing design (co-author of IEEE Proc. ReConFig 04, 05 and 06 papers), Synplicity and Steering Committee Int. Conf. on ReConFigurable Computing and FPGA's - ReConFig.
2006
Melhores Trabalhos SBCCI 2006, SBCCI.
2004
Woody Bledsoe Student Travel Award para apresentação de trabalho pelo aluno/orientando de doutorado Flávio C. de Moura no Doctoral Programme of the Second International Joint Conference on Automated Reasoning (IJCAR 2004), Cork, Ireland, Conference chairs and the CADE trustees.
2002
Prêmio de primeiro colocado no Seminário Sobre Novas Tecnologias no Ensino de Graduação na UnB: SAGEMoLiC - A Framework to Visualize Equivalences between Computational Models of Regular Languages, Decanato de Ensino e Graduação da Universidade de Brasília.
2002
Woody Bledsoe Student Travel Award para apresentação de trabalho pelo aluno/orientando de mestrado Rinaldi M. Neto no WRS'2002, Copenhagen, Denmark, Conference chairs and the CADE trustees.
2002
Orientação do Melhor Projeto da Área de Ciências Exatas. Aluno: Marcos de Andrade Gomes, PIBIC/CNPq/UnB.
1999
Orientação do Melhor Projeto da Área de Ciências Exatas. Aluno: Alison H. R. da Silva, PIBIC/CNPq/UnB.
1996
Paraninfo, Formandos em Ciência da Computação, Universidade de Brasília.
Histórico profissional
Endereço profissional
-
Universidade de Brasília, Instituto de Ciências Exatas. , Departamento de Ciência da Computação, Universidade de Brasília (UnB), Asa Norte, 70910900 - Brasília, DF - Brasil, Telefone: (61) 33073676, Fax: (61) 31073661, URL da Homepage:
Experiência profissional
2023 - Atual
Universidade Federal de GoiásVínculo: Colaborador, Enquadramento Funcional: PI em projetos de pesquisa, Carga horária: 5
Outras informações:
Cooperação em projetos coordenados no IME/UFG
2009 - Atual
Universidade de Brasília, UnBVínculo: Servidor Público, Enquadramento Funcional: Professor Titular em Ciência da Computação, Carga horária: 40, Regime: Dedicação exclusiva.
Outras informações:
Aprovado em concurso público em fevereiro 2009. Banca: Norai Rocco, Luiz F.G. Soares, Tomasz Kowaltowski, Cláudio L. Luccchesi, Ricardo A. L. Reis.
Posse como Professor Titular em Ciência da Computação em julho de 2009.
2008 - 2009
Universidade de Brasília, UnBVínculo: Servidor Público, Enquadramento Funcional: Professor Associado 2, Carga horária: 40, Regime: Dedicação exclusiva.
2006 - 2008
Universidade de Brasília, UnBVínculo: Servidor Público, Enquadramento Funcional: Professor Associado 1, Carga horária: 40, Regime: Dedicação exclusiva.
2001 - 2006
Universidade de Brasília, UnBVínculo: Servidor Público, Enquadramento Funcional: Professor Adjunto 4, Carga horária: 40, Regime: Dedicação exclusiva.
1999 - 2001
Universidade de Brasília, UnBVínculo: Servidor Público, Enquadramento Funcional: Professor Adjunto 3, Carga horária: 40, Regime: Dedicação exclusiva.
1997 - 1999
Universidade de Brasília, UnBVínculo: Servidor Público, Enquadramento Funcional: Professor Adjunto 2, Carga horária: 40, Regime: Dedicação exclusiva.
1995 - 1997
Universidade de Brasília, UnBVínculo: Servidor Público, Enquadramento Funcional: Professor Adjunto 1, Carga horária: 40, Regime: Dedicação exclusiva.
Outras informações:
Aprovado em concurso público em outubro de 1994.
Posse como Adjunto I em Janeiro de 1995. Banca: Said Sidki, Ruy de Queiroz e Norai Rocco
Atividades
-
01/2018
Conselhos, Comissões e Consultoria, Instituto de Ciências Exatas / Programa de Pós-graduação em Matemática.,Cargo ou função, Membro da Comissão de Pós-Graduação (Coordenador C. A. Pereira dos Santos).
-
01/2018
Conselhos, Comissões e Consultoria, Instituto de Ciências Exatas/Programa de Pós-Graduação em Inforrmática.,Cargo ou função, Membro da Comissão de Pós-graduação (Coordenador B.L. Macchiavello).
-
08/2009
Ensino, Ciência da Computação, Nível: Graduação,Disciplinas ministradas, Lógica Computacional (2009 II, 2010 I e II, 2011 I e II, 2012 I e II, 2013 I e II, 2014 I e II, 2015 I e II, 2016 I e II, 2017 I e II, 2018 I e II, 2019 I e II, 2020 I e II, 2021 I e II, 2022 I e II.)
-
01/2003
Ensino, Informática, Nível: Pós-Graduação,Disciplinas ministradas, Estágios de Pesquisa (05I,05II,06I,06II,07I,07II), Lógica Formal Computacional (2014 I, 2017 I), Projeto e Análise de Algoritmos 2 (11 II), Projeto e Complexidade de Algoritmos (03I), Seminário Vinculado (2010 I), Teoria da Computação (03II, 04II,05II, 08II, 10II, 11II, 12II, 13II, 14II, 15II, 16II, 17II, 18II, 19II, 20 II, 21 II, 22 II), Teoria de Prova (2016 I, 2019 I, 2021 I), Tópicos Avançados de Pesquisa em Informática: automação da terminação (2012 I), Tópicos Avançados de Pesquisa em Informática: Métodos Formais (Verão 2010, conjuntamente com Cesar Muñoz NASA Langley), Tópicos em Fundamentos e Métodos da Computação: Teoria de Prova (13 I), Tópicos em Fundamentos e Métodos da Computação: Teoria de Tipos (11 I, 14 I, 15 I), Tópicos em Fundamentos e Métodos de Computação: Análise de Algoritmos para Biocomputação (04I), Teoria de Tipos (18 I, 20 I, 22 I)
-
01/1996
Pesquisa e desenvolvimento, Instituto de Ciências Exatas, Departamento de Ciência da Computação.,Linhas de pesquisa
-
01/1995
Pesquisa e desenvolvimento, Instituto de Ciências Exatas, Departamento de Matemática.,Linhas de pesquisa
-
01/1995
Ensino, Matemática, Nível: Pós-Graduação,Disciplinas ministradas, Análise de Algoritmos e Estruturas de Dados (96I,97II), Complexidade Computacional e Computabilidade (05II, 2010I), Introdução à Computação: Fundamentos de Programação Funcional e Lógica (95II,97II,98II,00II,02II,03II), Linguagens Formais e Autômatos II (2007 I, 2012 I), Lógica Clássica e Extensões (2017 I), Seminário de Computação em Complexidade Computacional (97I), Seminário de Computação em Substituições Explícitas e Tipos Dependentes (05I,06II), Seminário de Computação em Teoria de Categorias e Computação (98II), Seminário de Computação em Teoria de Reescrita (94II), Seminário de Computação: Lógica, Semântica e Teoria da Computação (2006II, 2007II, 2008II, 2009II, 2010II, 2011II, 2012II, 2013II), Seminário de Computação (22I, 22II), Teoria de Complexidade e Computabilidade (01I, 10I), Tópicos em Computação: Lógica formal avançada (03II,05I,08I,09I), Tópicos em Computação: Teoria avançada de Tipos (02II), Tópicos em Computação: Teoria de Prova (06I, 09II, 16I, 19I, 21I), Tópicos em Computação: Teoria de Reescrita Avançada (2007II, 2008II, 2009II), Tópicos em Computação: Teoria de Tipos (02I,04II,18I, 20I, 22I)
-
12/2017 - 06/2019
Conselhos, Comissões e Consultoria, Instituto de Ciências Exatas.,Cargo ou função, Membro da Comissão Examinadora da Classe D - Progressão Funcional, Instituto de Ciências Exatas.
-
03/2013 - 05/2018
Conselhos, Comissões e Consultoria, Reitoria.,Cargo ou função, Membro IE da Banca Examinadora de Professor Associado (BEPA).
-
12/2014 - 11/2016
Conselhos, Comissões e Consultoria, Reitoria, Decanato de Pesquisa e Pós-Graduação.,Cargo ou função, Membro da Comissão de Reconhecimento de Diplomas (CRD) internacionais do Decanato de Pesquisa e Pós-Graduação da UnB..
-
09/2010 - 05/2016
Conselhos, Comissões e Consultoria, Reitoria, Decanato de Pesquisa e Pós-Graduação.,Cargo ou função, Membro da Câmara de Pesquisa e Pós-Graduação - representante do Instituto de Ciências Exatas.
-
08/2012 - 12/2015
Conselhos, Comissões e Consultoria, Instituto de Ciências Exatas/Programa de Pós-Graduação em Inforrmática.,Cargo ou função, Membro da Comissão de Pós-Graduação do Mestrado em Informática (Coordenadores: Prof. Mylène Queiroz, Prof. Ricardo Jacobi e Prof. Alba C.M.A. de Melo).
-
05/2010 - 05/2012
Direção e administração, Instituto de Ciências Exatas/Programa de Pós-Graduação em Inforrmática.,Cargo ou função, Coordenador de Programa.
-
01/1995 - 07/2009
Ensino, Matemática, Nível: Graduação,Disciplinas ministradas, Análise de Algoritmos (94II,95II,96II,98II,01II,02II,06II,08I,09I), Cálculo Diferencial e Integral (96II,98I,99I,01I,02I), Cálculo Numérico (95I,96I,03I,04I,05I), Linguagens Formais e Autômatos (94I,95I,98I,99I,02I,03I), Teoria dos Grafos (00II.01II)
-
08/2003 - 03/2009
Conselhos, Comissões e Consultoria, Instituto de Ciências Exatas, Departamento de Ciência da Computação.,Cargo ou função, Membro da Comissão de Pós-Graduação do Mestrado em Informática (Coordenadores: Prof. Li Weigang e Prof. Alba C.M.A. de Melo).
-
09/2005 - 09/2007
Direção e administração, Instituto de Ciências Exatas, Departamento de Matemática.,Cargo ou função, Coordenador do curso e Vice-Chefe de Departamento de Matemática (Chefe Prof. Nigel Pitt).
-
01/1996 - 12/2002
Ensino, Ciência da Computação, Nível: Pós-Graduação,Disciplinas ministradas, Projeto de Análise de Algoritmos (95II), Teoria da Computação (00II), Lógica Formal Aplicada (02II)
-
01/1996 - 08/1999
Conselhos, Comissões e Consultoria, Instituto de Ciências Exatas, Departamento de Matemática.,Cargo ou função, Membro da Comissão de Computação do Departamento de Matemática.
-
01/1998
Extensão universitária , Instituto de Ciências Exatas, Departamento de Matemática.,Atividade de extensão realizada, Docente na Especialização em Matemática para Administração e Economia (360 h).
-
01/1998
Conselhos, Comissões e Consultoria, Decanato de Pesquisa e Pós-Graduação.,Cargo ou função, Membro Comitê Interno PIBIC-UnB/CNPq - Programa de Iniciação Científica.
-
08/1996 - 07/1998
Conselhos, Comissões e Consultoria, Instituto de Ciências Exatas / Programa de Pós-graduação em Matemática.,Cargo ou função, Membro da Comissão de Pós-Graduação do Departamento de Matemática (Coordenador J.V.Gonçalves).
-
01/1997
Outras atividades técnico-científicas , Instituto de Ciências Exatas, Instituto de Ciências Exatas.,Atividade realizada, Participação em projeto PROIN/CAPES para modernização do ensino do cálculo.
-
01/1997
Outras atividades técnico-científicas , Instituto de Ciências Exatas, Instituto de Ciências Exatas.,Atividade realizada, Coordenador da "Escola de Verão". Projeto institucional CNPq 453687/96-2 com recursos adicionais da CAPES, FINEP e COLCIENCIAS.
2003 - Atual
Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPqVínculo: Bolsista, Enquadramento Funcional: Bolsista Produtividade, Carga horária: 20
2003 - Atual
Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPqVínculo: Colaborador, Enquadramento Funcional: Consultor-Assessor
Outras informações:
Consultor Ad-Hoc e membro de diversos Comitês de Assessoramento e Seleção, entre outros bolsas DAAD/CNPq/CAPES, RHAE, e de Cooperação Internacional.
1994 - 1995
Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPqVínculo: Bolsista, Enquadramento Funcional: Bolsista Recém Doutor, Regime: Dedicação exclusiva.
2001 - Atual
Coordenação de Aperfeiçoamento de Pessoal de Nível SuperiorVínculo: Colaborador, Enquadramento Funcional: Consultor-Assesor
Outras informações:
Consultor ad hoc e membro de diversos comitês de assessoramento, entre outros DAAD/CAPES/CNPq, e editais de cooperação internacional.
1999 - 2000
Coordenação de Aperfeiçoamento de Pessoal de Nível SuperiorVínculo: Bolsista, Enquadramento Funcional: Pesq. Associado Heriot-Watt U. Edimburgo U.K., Regime: Dedicação exclusiva.
Outras informações:
Pesquisador Associado no ULTRA group da Heriot-Watt University, Edimburgo, Escócia. Afastado da Universidade de Brasília.
2001 - Atual
Fundação de Apoio à Pesquisa do Distrito FederalVínculo: Consultor-Assessor, Enquadramento Funcional: Consultor-Assessor
Outras informações:
Consultor Ad-Hoc e membro de diversos Comitês de Assessoramento.
2002 - 2002
Fundação de Estudos em Ciências MatemáticasVínculo: Bolsista, Enquadramento Funcional: Pesquisador, Carga horária: 20
Outras informações:
Bolsista de pesquisa do programa de incentivo à pesquisa da Fundação de Estudos em Ciências Matemáticas. Projeto: "Cálculos de substituições explícitas e unificação de ordem superios - O caso dos padrões de ordem superior". Departamento de Matemática, Instituto de Ciências Exatas, UnB.
1999 - 1999
Fundação de Estudos em Ciências MatemáticasVínculo: Bolsista, Enquadramento Funcional: Pesquisador, Carga horária: 20
Outras informações:
Bolsista de Pesquisa do programa de incentivo à produção científica da Fundação de Estudos em Ciências Matemáticas. Projeto: "Teoria de Reescrita, Teoria de Tipos e Problemas de Unificação Aritmética". Departamento de Matemática, Instituto de Ciências Exatas, UnB.
2019 - 2019
KINGS COLLEGEVínculo: Professor Visitante, Enquadramento Funcional: Professor Visitante, Carga horária: 40
Outras informações:
Pesquisa conjunta com a Professora Maribel Fernández na área de sintaxe nominal e questões equacionais .
2018 - 2018
KINGS COLLEGEVínculo: Professor Visitante, Enquadramento Funcional: Pesquisador visitante, Carga horária: 40
Outras informações:
Pesquisa em unificação nominal junto à Professora Maribel Fernández
2017 - 2017
KINGS COLLEGEVínculo: Professor Visitante, Enquadramento Funcional: Pesquisador visitante, Carga horária: 40
Outras informações:
Missão de pesquisa em sistemas nominais junto à pesquisadora Professora Maribel Fernández. Co-orientação Washington Luis Ribeiro de Carvalho Segundo.
2015 - 2015
KINGS COLLEGEVínculo: Professor Visitante, Enquadramento Funcional: Pesquisador visitante, Carga horária: 40
Outras informações:
Pesquisa conjunta em formalização de propriedades de sistemas nominais (unificação nominal) e tipos de intersecção em sistemas nominais. Responsável Prof. Maribel Fernández. Co-orientação Ana Cristina Rocha Oliveira.
2015 - 2015
KINGS COLLEGEVínculo: Professor Visitante, Enquadramento Funcional: Pesquisador visitante, Carga horária: 40
Outras informações:
Pesquisa conjunta em formalização de propriedades de sistemas nominais, tipos de intersecção em sistemas nominais e equivalência em sintaxe nominal módulo teorias equacionais. Responsável Prof. Maribel Fernández.
2012 - 2012
KINGS COLLEGEVínculo: Professor vistante, Enquadramento Funcional: Pesquisador visitante, Carga horária: 40
Outras informações:
Visita de cooperação em aplicação de sistemas de reescrita e dedutivos a análise criptográfico. Responsável Prof. Maribel Fernández. Co-orientação Daniele Nantes.
2011 - 2011
KINGS COLLEGEVínculo: Professor vistante, Enquadramento Funcional: Pesquisador visitante, Carga horária: 40
Outras informações:
Visita de cooperação em pesquisa em reescrita e sistemas dedutivos aplicados em criptografia. Responsável Prof. Maribel Fernández. Co-orientação Daniele Nantes.
2015 - 2015
National Institute of AerospaceVínculo: Professor Visitante, Enquadramento Funcional: pesquisador visitante, Carga horária: 40
Outras informações:
Pesquisa conjunta em formalização de correção de mecanismos de automação da terminação. Responsável Cesar Muñoz (NASA Langley). Colaboração Mariano Moscatto (NIA).
2012 - 2012
National Institute of AerospaceVínculo: Professor Visitante, Enquadramento Funcional: pesquisador visitante, Carga horária: 40
Outras informações:
Pesquisa conjunta em formalização de teoremas de correção do princípio de mudança de tamanho aplicada em automação da terminação. Responsável Cesar Muñoz (NASA Langley). Co-orientação Andréia Borges Avelar.
2011 - 2011
National Institute of AerospaceVínculo: Professor Visitante, Enquadramento Funcional: Pesquisador visitante, Carga horária: 40
Outras informações:
Visita para pesquisa em terminação em PVS. conjuntamente com Cesar Muñoz (NASA Langley) e Alwyn Goodloe (NIA-NASA Langley).
2010 - 2010
National Institute of AerospaceVínculo: Professor vistante, Enquadramento Funcional: Consultor, Carga horária: 20
Outras informações:
Pesquisa e implementação em PVS de técnicas de automação da terminação utilizando o princípio de mudança de tamanho (size-change principle) conjuntamente com Cesar Muñoz (NASA Langley) e Alwyn Goodloe (NIA-NASA Langley).
2010 - 2010
Uni-Karlsruhe - Universität Karlsruhe (TH) ,Vínculo: Professor Visitante, Enquadramento Funcional: Pesquisador Visitante, Regime: Dedicação exclusiva.
Outras informações:
Visita científica ao ITIV - Institut für Technik der Informationsverarbeitung, em projeto CNPq/DFG.
Short course on Formal Methods Applied to the Implementation of Secure Software/Hardware using PVS.
2008 - 2008
Uni-Karlsruhe - Universität Karlsruhe (TH) ,Vínculo: Professor vistante, Enquadramento Funcional: Pesquisador Visitante, Regime: Dedicação exclusiva.
Outras informações:
Visita científica ao ITIV - Institut für Technik der Informationsverarbeitung, em projeto CNPq/DFG.
2004 - 2004
Uni-Karlsruhe - Universität Karlsruhe (TH) ,Vínculo: Professor vistante, Enquadramento Funcional: Pesquisador Visitante
Outras informações:
Visita científica ao ITIV - Institut für Technik der Informationsverarbeitung, em projeto CAPES/DFG.
2002 - 2002
Uni-Karlsruhe - Universität Karlsruhe (TH) ,Vínculo: Professor vistante, Enquadramento Funcional: Pesquisador Visitante, Regime: Dedicação exclusiva.
Outras informações:
Visita científica ao ITIV - Institut für Technik der Informationsverarbeitung, em projeto CAPES/DFG.
2002 - 2002
Universitaet KaiserslauternVínculo: Pesquisador visitante, Enquadramento Funcional: Pesquisador Visitante, Carga horária: 40
Outras informações:
Pesquisa no contexto de projeto de colaboração CAPES/DFG junto aos Profs. Reiner W. Hartenstein (Universitaet Kaiserslautern) e Juergen Becker (ITIV, Universitaet Karlsruhe)
1990 - 1991
Universitaet KaiserslauternVínculo: Colaborador, Enquadramento Funcional: Assistente de Ensino, Carga horária: 8
Atividades
-
05/2002 - 05/2002
Pesquisa e desenvolvimento, Fachbereich Informatik, Ag Computer Systems.,Linhas de pesquisa
-
03/1990 - 09/1991
Ensino, Fachbereich Informatik, Nível: Graduação,Disciplinas ministradas, Algoritmos Eficientes, Especificação Algébrica
2005 - 2005
Technische Universitaet MuenchenVínculo: Pesquisador visitante, Enquadramento Funcional: Theorem Provin Group, Tobias Nipkow, Regime: Dedicação exclusiva.
Outras informações:
Financiamento Deutscher Akademischer Austauschsdients - DAAD
2001 - 2010
Heriot-Watt UniversityVínculo: Colaborador, Enquadramento Funcional: Affiliate Member, Carga horária: 4
Outras informações:
Diversas visitas e cooperação contínua em pesquisa com membros do grupo ULTRA (Useul Logics, Types, Rewriting, and their Automation) liderado pela Prof. Fairouz Kamareddine
2008 - 2008
Heriot-Watt UniversityVínculo: Professor Visitante, Enquadramento Funcional: Pesquisador visitante, Carga horária: 40
Outras informações:
Visita de cooperação e pesquisa conjunta em cálculos de substituições explícitas com Prof. Fairouz Kamareddine. Co-orientação Daniel Lima Ventura.
2007 - 2007
Heriot-Watt UniversityVínculo: Professor Visitante, Enquadramento Funcional: Pesquisador visitante, Carga horária: 40
Outras informações:
Visita de cooperação e pesquisa conjunta em cálculos de substituições explícitas com Prof. Fairouz Kamareddine. Co-orientação Daniel Lima Ventura.
2005 - 2005
Heriot-Watt UniversityVínculo: Professor Visitante, Enquadramento Funcional: Pesquisador visitante, Carga horária: 40
Outras informações:
Visita de cooperação e pesquisa conjunta em cálculos de substituições explícitas com Prof. Fairouz Kamareddine. Co-orientação Flávio L.C. de Moura.
2004 - 2004
Heriot-Watt UniversityVínculo: Professor Visitante, Enquadramento Funcional: Pesquisador visitante, Carga horária: 40
Outras informações:
Visita de cooperação e pesquisa conjunta em cálculos de substituições explícitas com Prof. Fairouz Kamareddine. Co-orientação Flávio L.C. de Moura.
2003 - 2003
Heriot-Watt UniversityVínculo: Professor Visitante, Enquadramento Funcional: Pesquisador visitante, Carga horária: 40
Outras informações:
Visita de cooperação e pesquisa conjunta em cálculos de substituições explícitas com Prof. Fairouz Kamareddine.
1999 - 2000
Heriot-Watt UniversityVínculo: Pesquisador visitante, Enquadramento Funcional: Pesquisador Associado, Regime: Dedicação exclusiva.
Outras informações:
Pesquisador visitante, bolsista de pós-doutorado com financiamento da CAPES no Grupo ULTRA,
Computer & Electrical Engineering
2002 - 2003
Kluwer Academic PublishersVínculo: Revisor, Enquadramento Funcional:
Outras informações:
Thirty Five Years of Automating Mathematics, dedicated to 35 years of N.G. de Bruijn´s Automath. Kluwer Applied Logic Series, Fairouz Kamareddine Ed., Julho 2003.
1987 - 1988
Escuela Colombiana de IngenieríaVínculo: Professor Auxiliar, Enquadramento Funcional: Professor Auxiliar, Carga horária: 8
Atividades
-
01/1987 - 06/1988
Ensino, Departamento de Ingeniería de Sistemas y Computaci, Nível: Graduação,Disciplinas ministradas, Matemática Estrutural para Ciência da Computação 1 (1987/I, 1988/I), Fundamentos de Inteligência Artificial (1987/II, 1988/I), Matemática Estructural para Ciência da Computação 2 (1987/II)
1986 - 1986
Fundação Universidad Autónoma de ManizalesVínculo: Professor Auxiliar, Enquadramento Funcional: Professor Auxiliar, Carga horária: 40
Atividades
-
07/1986 - 12/1986
Ensino, Facultad de Ingeniería de Sistemas y Computación, Nível: Graduação,Disciplinas ministradas, Análise de Algoritmos, Estructuras de Dados, Linguagens de Programação
1986 - 1988
Universidad de Los AndesVínculo: Professor Auxiliar, Enquadramento Funcional: Assistente de Ensino, Carga horária: 16
1985 - 1985
Universidad de Los AndesVínculo: Prática de Ensino, Enquadramento Funcional: Assistente de ensino, Carga horária: 12
Atividades
-
01/1985 - 09/1988
Ensino, Departamentos de Matemáticas e Ingeniería de Siste, Nível: Graduação,Disciplinas ministradas, Álgebra Linear (Verão 1985), Cálculo de Sucessões e Séries (1986/I), Cálculo Diferencial e Integral (1985/II, 1987/I,1987/II,1988/I), Cálculo Vetorial (Verão 1988), Introdução à Computação (1985 II), Lições de Geometria (1988/I), Pré-cálculo (1985/I,1987/I,Verão 1987,1987/II)
2025 - 2025
Universidad Nacional de Colombia - ManizalesVínculo: Professor Visitante, Enquadramento Funcional: Professor Visitante Sênior, Carga horária: 40
Outras informações:
Pesquisa em formalização computacional de teoremas combinatórios sobre estruturas infinitas. Em cooperação com pesquisadores da UNAL e da UFG.
2018 - 2018
Universidad Nacional de Colombia - ManizalesVínculo: Professor Visitante, Enquadramento Funcional: Professor Visitante Sênior, Carga horária: 40
Outras informações:
Professor Visitante, Facultad de Ciencias Exactas y Naturales, Departamento de Matemáticas junto ao Professor Fabian Serrano. Realização de atividades de pesquisa em lógica e formalização e de curso intensivo en Sistemas Deductivos y Eliminação da Regra de Corte.
2017 - 2017
Universidad Nacional de Colombia - ManizalesVínculo: Professor Visitante, Enquadramento Funcional: Professor Visitante Sênior, Carga horária: 20
Outras informações:
Professor Visitante, Facultad de Ciencias Exactas y Naturales, Departamento de Matemáticas junto ao Professor Fabian Serrano. Realização de atividades de pesquisa em lógica e formalização e de curso intensivo en Lógica Matemática y Computacional para alumnos del curso de Matemáticas.
2015 - Atual
American Mathematical SocietyVínculo: Reviewer Mathematical Reviews, Enquadramento Funcional: Revisor da base AMS MathSciNet, Carga horária: 2
Outras informações:
The Mathematical Reviews Database, MathSciNet, covers the world of
research literature in mathematics by means of reviews written by subject
experts.
2024 - 2025
Research Institute for Symbolic Computation / Johannes Kepler UniversitätVínculo: Professor Visitante, Enquadramento Funcional: Professor Visitante Sênior - CAPES PrInt, Carga horária: 40, Regime: Dedicação exclusiva.
Outras informações:
Pesquisa conjunta em formalização de algoritmos de anti-unificação com participação de colegas de diversas instituições e alunos de doutorado do PPG em Matemática da Universidade de Brasília.
Propriedade Intelectual
Patentes (1)
| Tipo | Título | Data depósito |
|---|---|---|
| INVENTOR | Sistema de controle distribuído de grupo de elevadores usando dispositivos reconfiguráveis | 02/07/2008 |
Criando um monitoramento
Nossos robôs irão buscar nos nossos bancos de dados todos os processos de Mauricio Ayala Rincon e sempre que o nome aparecer em publicações dos Diários Oficiais, avisaremos por e-mail e pelo painel do usuário
Criando um monitoramento
Nossos robôs irão buscar nos nossos bancos de dados todas as movimentações desse processo e sempre que o processo aparecer em publicações dos Diários Oficiais e nos Tribunais, avisaremos por e-mail e pelo painel do usuário
Confirma a exclusão?