Mauricio Ayala Rincon

Bolsista de Produtividade em Pesquisa do CNPq - Nível 1D

  • Endereço para acessar este CV: http://lattes.cnpq.br/8466420403941522
  • Última atualização do currículo em 06/10/2018


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 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 sendo co-chair do PC deste último em 2006, 2007, 2009 e 2014. 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. Foi co-chair da conferência "8th Interactive Theorem Proving" (ITP 2017) e membro ex-officio do Steering Committee de ITP (2017-18). Foi co-chair do "32nd International Workshop on Unification" (UNIF 2018) afiliado a FSCD/FLOC 2018 e, é co-chair do "8th International Workshop on Confluence" (IWC 2019). (Texto informado pelo autor)


Identificação


Nome
Mauricio Ayala Rincon
Nome em citações bibliográficas
M. Ayala-Rincón;AYALARINCON, M;Ayala-Rincon, M.;Ayala-Rincón, Mauricio;AYALA-RINCON, MAURICIO;AYALA-RINC´N, MAURICIO;AYALA-RINC'N, MAURICIO

Endereço


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: www.mat.unb.br/~ayala


Formação acadêmica/titulação


1989 - 1993
Doutorado em Fachbereich Informatik.
Universitaet Kaiserslautern, UNIKL, Alemanha.
Título: Expressiveness of Conditional Rewriting Systems with Built-in Predicates, Ano de obtenção: 1993.
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
1981 - 1987
Graduação em Matemática.
Universidad de Los Andes, UNIANDES, Colômbia.
Título: Algunos Aspectos de la Teoria de Bifurcaciones.
Orientador: Prof Dr. rer. nat. Jaime Lesmes.
1980 - 1985
Graduação em Ingeniería de Sistemas y Computación.
Universidad de Los Andes, UNIANDES, Colômbia.
Título: Generador de Evaluadores para Gramáticas con Atributos Fuertemente No-Circulares.
Orientador: Prof Dr. Rodrigo Lopez.


Pós-doutorado


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.


Atuação Profissional



Universidade de Brasília, UnB, Brasil.
Vínculo institucional

2009 - Atual
Ví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.

Vínculo institucional

2008 - 2009
Vínculo: Servidor Público, Enquadramento Funcional: Professor Associado 2, Carga horária: 40, Regime: Dedicação exclusiva.

Vínculo institucional

2006 - 2008
Vínculo: Servidor Público, Enquadramento Funcional: Professor Associado 1, Carga horária: 40, Regime: Dedicação exclusiva.

Vínculo institucional

2001 - 2006
Vínculo: Servidor Público, Enquadramento Funcional: Professor Adjunto 4, Carga horária: 40, Regime: Dedicação exclusiva.

Vínculo institucional

1999 - 2001
Vínculo: Servidor Público, Enquadramento Funcional: Professor Adjunto 3, Carga horária: 40, Regime: Dedicação exclusiva.

Vínculo institucional

1997 - 1999
Vínculo: Servidor Público, Enquadramento Funcional: Professor Adjunto 2, Carga horária: 40, Regime: Dedicação exclusiva.

Vínculo institucional

1995 - 1997
Ví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

12/2017 - Atual
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.
08/2009 - Atual
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)
1/2003 - Atual
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)
Teoria de Prova (2016 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, 18 I)
Tópicos em Fundamentos e Métodos de Computação: Análise de Algoritmos para Biocomputação (04I)
01/1996 - Atual
Pesquisa e desenvolvimento , Instituto de Ciências Exatas, Departamento de Ciência da Computação.

1/1995 - Atual
Pesquisa e desenvolvimento , Instituto de Ciências Exatas, Departamento de Matemática.

1/1995 - Atual
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)
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)
Tópicos em Computação: Teoria de Reescrita Avançada (2007II, 2008II, 2009II)
Tópicos em Computação: Teoria de Tipos (02I,04II,18I)
3/2013 - 5/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.
8/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 - 5/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.
1/1995 - 7/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)
8/2003 - 3/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).
9/2005 - 9/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)
1/1996 - 8/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.
1998 - 1999
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).
1998 - 1999
Conselhos, Comissões e Consultoria, Instituto de Ciências Exatas, .

Cargo ou função
Membro Comitê Interno PIBIC-UnB/CNPq - Programa de Iniciação Cinetífica.
8/1996 - 7/1998
Conselhos, Comissões e Consultoria, Instituto de Ciências Exatas, Departamento de 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).
1997 - 1998
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.
1997 - 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.

Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPq, Brasil.
Vínculo institucional

2003 - Atual
Vínculo: Bolsista, Enquadramento Funcional: Bolsista Produtividade, Carga horária: 20

Vínculo institucional

2003 - Atual
Ví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.

Vínculo institucional

1994 - 1995
Vínculo: Bolsista, Enquadramento Funcional: Bolsista Recém Doutor, Regime: Dedicação exclusiva.


Coordenação de Aperfeiçoamento de Pessoal de Nível Superior, CAPES, Brasil.
Vínculo institucional

2001 - Atual
Ví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.

Vínculo institucional

1999 - 2000
Ví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.


Fundação de Apoio à Pesquisa do Distrito Federal, FAP/DF, Brasil.
Vínculo institucional

2001 - Atual
Vínculo: Consultor-Assessor, Enquadramento Funcional: Consultor-Assessor
Outras informações
Consultor Ad-Hoc e membro de diversos Comitês de Assessoramento. Atualmente membro da Comitê de Assessoramento Técnico Científico por resolução do Conselho Superior da FAP DF DO/DF No 82, 2/4/2014, p. 21-22.


Fundação de Estudos em Ciências Matemáticas, FEMAT, Brasil.
Vínculo institucional

2002 - 2002
Ví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.

Vínculo institucional

1999 - 1999
Ví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.


KINGS COLLEGE, KCL, Inglaterra.
Vínculo institucional

2018 - 2018
Vínculo: Professor Visitante, Enquadramento Funcional: Pesquisador visitante, Carga horária: 40
Outras informações
Pesquisa em unificação nominal junto à Professora Maribel Fernández

Vínculo institucional

2017 - 2017
Ví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.

Vínculo institucional

2015 - 2015
Ví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.

Vínculo institucional

2015 - 2015
Ví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.

Vínculo institucional

2012 - 2012
Ví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.

Vínculo institucional

2011 - 2011
Ví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.


National Institute of Aerospace, NIA, Estados Unidos.
Vínculo institucional

2015 - 2015
Ví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).

Vínculo institucional

2012 - 2012
Ví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.

Vínculo institucional

2011 - 2011
Ví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).

Vínculo institucional

2010 - 2010
Ví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).


Uni-Karlsruhe - Universität Karlsruhe (TH) ,, UK, Alemanha.
Vínculo institucional

2010 - 2010
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.

Vínculo institucional

2008 - 2008
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.

Vínculo institucional

2004 - 2004
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.

Vínculo institucional

2002 - 2002
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.


Universitaet Kaiserslautern, UNIKL, Alemanha.
Vínculo institucional

2002 - 2002
Ví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)

Vínculo institucional

1990 - 1991
Vínculo: Colaborador, Enquadramento Funcional: Assistente de Ensino, Carga horária: 8

Atividades

5/2002 - 5/2002
Pesquisa e desenvolvimento , Fachbereich Informatik, Ag Computer Systems.

3/1990 - 9/1991
Ensino, Fachbereich Informatik, Nível: Graduação

Disciplinas ministradas
Algoritmos Eficientes
Especificação Algébrica

Technische Universitaet Muenchen, TUM, Alemanha.
Vínculo institucional

2005 - 2005
Vínculo: Pesquisador visitante, Enquadramento Funcional: Theorem Provin Group, Tobias Nipkow, Regime: Dedicação exclusiva.
Outras informações
Financiamento Deutscher Akademischer Austauschsdients - DAAD


Heriot-Watt University, HWU, Grã-Bretanha.
Vínculo institucional

2001 - 2010
Ví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

Vínculo institucional

2008 - 2008
Ví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.

Vínculo institucional

2007 - 2007
Ví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.

Vínculo institucional

2005 - 2005
Ví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.

Vínculo institucional

2004 - 2004
Ví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.

Vínculo institucional

2003 - 2003
Ví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.

Vínculo institucional

1999 - 2000
Ví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


Kluwer Academic Publishers, KLUWER, Holanda.
Vínculo institucional

2002 - 2003
Ví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.


Escuela Colombiana de Ingeniería, ESCOLING, Colômbia.
Vínculo institucional

1987 - 1988
Vínculo: Professor Auxiliar, Enquadramento Funcional: Professor Auxiliar, Carga horária: 8

Atividades

1/1987 - 6/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)

Fundação Universidad Autónoma de Manizales, FUAMA, Colômbia.
Vínculo institucional

1986 - 1986
Vínculo: Professor Auxiliar, Enquadramento Funcional: Professor Auxiliar, Carga horária: 40

Atividades

7/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

Universidad de Los Andes, UNIANDES, Colômbia.
Vínculo institucional

1986 - 1988
Vínculo: Professor Auxiliar, Enquadramento Funcional: Assistente de Ensino, Carga horária: 16

Vínculo institucional

1985 - 1985
Vínculo: Prática de Ensino, Enquadramento Funcional: Assistente de ensino, Carga horária: 12

Atividades

1/1985 - 9/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)

Universidad Nacional de Colombia - Manizales, UNAL - MANIZALES, Colômbia.
Vínculo institucional

2018 - 2018
Vínculo: Professor Visitante, Enquadramento Funcional: Professor visitante, 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.

Vínculo institucional

2017 - 2017
Vínculo: Professor Visitante, Enquadramento Funcional: Professor Visitante, 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.



Linhas de pesquisa


1.
Aplicações da teoria de reescrita
2.
Animação de algoritmos e visualização
3.
Teoria de reescrita, reescrita-lógica e aplicações
4.
Computação eficiente para processamento de seqüências
5.
Cálculo lambda e cálculos de substituições explícitas
6.
Análise de Algoritmos
7.
Dedução Automática baseada em técnicas de reescrita
8.
Especificação Algébrica
9.
Sistemas de Reescrita
10.
Teoria dos Tipos
11.
Substituições Explícitas
12.
Verficação formal
13.
Sintaxe nominal
14.
Aplicações da teoria da reescrita no desenvolvimento de hardware


Projetos de pesquisa


2017 - Atual
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..
Situação: Em andamento; 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 / 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.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: 5 / Número de orientações: 4
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.
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 orientações: 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 orientações: 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.
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: 3 / Número de orientações: 1
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 / Conselho Nacional de Desenvolvimento Científico e Tecnológico - Bolsa / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - Bolsa.
Número de produções C, T & A: 12 / Número de orientações: 8
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.


Outros Projetos


2001 - 2004
Coordenador brasileiro do projeto CAPES/DFG 009-1 Aplicação da teoria de reescrita no projeto de hardware reconfigurável. Coordenador alemão Reiner W. Hartenstein. UnB, UFRGS,ITIV Universität Karlsruhe, Universität Kaiserslautern.
Descrição: Exploração da alplicabilidade da teoria de reescrita-lógica no desenho de hardware reconfigurável e a sua adequação na implementação eficiente de soluções para problemas algébricos, combinatórios sobre palavras e seqüências e computacionais, em geral. Equipe alemão: Prof. Jürgen Becker, Diretor Institut für Technik der Informationsverarbeitung; Universität Karlsruhe; Prof. Reiner W. Hartenstein, Universität Kaiserslautern (Coordenador do time alemão); Prof. Ricardo Reis, UFRGS; Prof. Sergio Bampi, UFRGS; Prof. Ricardo P. Jacobi, UnB; Prof. Carlos H. Llanos, UnB. Resultados parciais: publicações em congressos e períodicos referenciados internacionais e nacionais; duas dissertações de mestrado; tês projetos PIBIC; implementação de duas orientações no nível de doutorado..
Situação: Concluído; Natureza: Outra.
Alunos envolvidos: Graduação: (3) / Especialização: (0) / Mestrado acadêmico: (3) / Mestrado profissional: (0) / Doutorado: (1) .
Integrantes: Mauricio Ayala Rincon - Coordenador / Rodrigo Borges Nogueira - Integrante / Reiner W Hartenstein - Integrante / Ricardo P Jacobi - Integrante / Carlos Llanos - Integrante / Felipe Paulino Tavares - Integrante / Wander Jácome de Queiroz - Integrante / Luis G A Carvalho - Integrante / Jürgen Becker - Integrante / Ricardo A L Reis - Integrante / Sergio Bampi - Integrante.Financiador(es): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - Auxílio financeiro / Deutsche Forschung Gemeinschaft - Auxílio financeiro.
Número de produções C, T & A: 6 / Número de orientações: 3


Membro de corpo editorial


1999 - Atual
Periódico: Revista Colombiana de Computación


Membro de comitê de assessoramento


2014 - Atual
Agência de fomento: Fundação de Apoio à Pesquisa do Distrito Federal


Revisor de periódico


2006 - 2007
Periódico: Journal of Algorithms
2018 - Atual
Periódico: Theoretical Computer Science
2004 - Atual
Periódico: Theoretical Computer Science
2001 - 2001
Periódico: The Computer Journal
2000 - 2001
Periódico: Journal of Symbolic Computation
2018 - Atual
Periódico: Journal of Automated Reasoning
2011 - 2013
Periódico: Journal of Automated Reasoning
2003 - 2004
Periódico: Journal of Automated Reasoning
2002 - 2013
Periódico: Journal of Automated Reasoning
1999 - 2000
Periódico: Journal of Logic and Computation
2008 - 2009
Periódico: The Logical Journal of the Interst Group on Applied Logic
1996 - 2009
Periódico: The Logical Journal of the Interst Group on Applied Logic
2009 - 2009
Periódico: Ars Combinatoria
2011 - 2011
Periódico: JICS. Journal of Integrated Circuits and Systems (Ed. Português)
2010 - 2011
Periódico: JICS. Journal of Integrated Circuits and Systems (Ed. Português)
2010 - 2010
Periódico: Journal of Signal Processing Systems
2012 - 2012
Periódico: Digital Signal Processing (Print)
2011 - 2013
Periódico: Journal of the Brazilian Computer Society (Impresso)
2011 - 2012
Periódico: ACM Transactions on Reconfigurable Technology and Systems
2008 - 2009
Periódico: Logic Journal of the IGPL (Print)
2008 - 2009
Periódico: Mechatronics (Oxford)
2010 - 2011
Periódico: Theoretical Computer Science
2014 - 2014
Periódico: International Journal of Computer Mathematics
2014 - 2015
Periódico: International Journal of Algebra and Computation
2015 - 2015
Periódico: IEEE Transactions on Parallel and Distributed Systems (Print)
2015 - 2015
Periódico: International Journal of Reconfigurable Computing (Print)
2015 - 2016
Periódico: Computacion y Sistemas
2016 - 2016
Periódico: Microprocessors and Microsystems
2015 - 2016
Periódico: Computacion y Sistemas
2016 - 2016
Periódico: International Journal of Engineering, Science and Technology
2017 - Atual
Periódico: IEEE Transactions on Evolutionary Computation
2018 - Atual
Periódico: MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE


Revisor de projeto de fomento


2017 - 2017
Agência de fomento: Agencia Nacional de Investigación e Innovación
2014 - 2014
Agência de fomento: Fundação de Amparo à Pesquisa do Estado de Minas Gerais
2012 - Atual
Agência de fomento: Fonds zur Förderung der wissenschaftlichen Forschung
2012 - 2012
Agência de fomento: Fundação de Apoio à Pesquisa do Estado do Rio Grande do Norte
2011 - 2016
Agência de fomento: Fundação de Amparo à Pesquisa do Estado da Bahia
2009 - 2009
Agência de fomento: Fundação de Amparo à Pesquisa do Estado do Rio Grande do Sul
2002 - 2017
Agência de fomento: Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco
2001 - 2001
Agência de fomento: Fundação de Amparo à Pesquisa do Estado de São Paulo


Áreas de atuação


1.
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação.
2.
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.
3.
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.
4.
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.
5.
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.
6.
Grande área: Ciências Exatas e da Terra / Área: Matemática / Subárea: Matemática Aplicada.


Idiomas


Alemão
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.
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.


Prêmios e títulos


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" RTA, 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.


Produções



Produção bibliográfica
Citações

Web of Science
Total de trabalhos:75
Total de citações:113
Fator H:6
Ayala-Rincon, Mauricio  Data: 31/08/2018

SCOPUS
Total de trabalhos:99
Total de citações:397
Ayala-Rincon, M (Scopus: H-index 11)  Data: 07/05/2018

Outras
Total de trabalhos:140
Total de citações:976
Ayala-Rincon, M (Google Scholar: H-index 17, i10-Index 42)  Data: 07/05/2018

Artigos completos publicados em periódicos

1.
DE LIMA, THAYNARA ARIELLY2018DE 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.

2.
M. Ayala-Rincón2018M. Ayala-Rincón; FERNANDEZ, M. ; Rocha Oliveira, Ana Cristina ; VENTURA, Daniel Lima . Nominal essential intersection types. THEORETICAL COMPUTER SCIENCE, p. 62-80, 2018.

3.
ROCHA-OLIVEIRA, ANA CRISTINA2017ROCHA-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.

4.
Ayala-Rincón, Mauricio2017Ayala-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.

5.
Ayala-Rincón, Mauricio2017Ayala-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.

6.
Ayala-Rincón, Mauricio2016Ayala-Rincón, Mauricio. Formalising Confluence in PVS. Electronic Proceedings in Theoretical Computer Science, v. 204, p. 11-17, 2016.

7.
Ayala-Rincón, Mauricio2016Ayala-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.

8.
Ayala-Rincón, Mauricio2016Ayala-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.

9.
VISO, ANDRÉS2016VISO, 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.

10.
NOGUEIRA NUNES, DANIEL SAAD2016NOGUEIRA 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.

11.
Soncco-Álvarez, J.L.2015Soncco-Á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.

12.
VENTURA, D. L.2015VENTURA, 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.

13.
NUNES, D. S. N.2014NUNES, 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.

14.
Avelar, Andréia B2014Avelar, 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.

15.
MUÑOZ, DANIEL M.2014MUÑ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.

16.
Soncco-Álvarez, J.L.2013Soncco-Á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.

17.
Rocha Oliveira, Ana Cristina2013Rocha 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.

18.
Ayala-Rincón, Mauricio2013Ayala-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.

19.
Santos Rego, Yuri2013Santos 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.

20.
Avelar, Andréia B2012Avelar, 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.

21.
de Moura, F.L.C.2011de 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.

22.
ARBOLEDA, Daniel Muñoz2010ARBOLEDA, 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.

23.
Galdino, André L.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.

24.
Ventura, D.2009Ventura, 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.

25.
Galdino, André L.2009Galdino, 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.

26.
MOURA, Flávio Leonardo Cavalcanti de2008MOURA, 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.

27.
ARBOLEDA, Daniel Muñoz2008ARBOLEDA, 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.

28.
GALDINO, André Luiz2008GALDINO, 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.

29.
GALDINO, André Luiz2008GALDINO, André Luiz ; AYALARINCON, M . A Theory for Abstract Reduction Systems in PVS. CLEI Electronic Journal, v. 11, p. 1-12, 2008.

30.
BOUKERCHE, Azzedine2007BOUKERCHE, 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.

31.
M. Ayala-Rincón;AYALARINCON, M;Ayala-Rincon, M.;Ayala-Rincón, Mauricio;AYALA-RINCON, MAURICIO;AYALA-RINC´N, MAURICIO;AYALA-RINC'N, MAURICIO2007M. 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.

32.
BOUKERCHE, Azzedine2007BOUKERCHE, 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.

33.
M. Ayala-Rincón;AYALARINCON, M;Ayala-Rincon, M.;Ayala-Rincón, Mauricio;AYALA-RINCON, MAURICIO;AYALA-RINC´N, MAURICIO;AYALA-RINC'N, MAURICIO2006M. 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.

34.
MOURA, Flávio Leonardo Cavalcanti de2006MOURA, 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.

35.
M. Ayala-Rincón;AYALARINCON, M;Ayala-Rincon, M.;Ayala-Rincón, Mauricio;AYALA-RINCON, MAURICIO;AYALA-RINC´N, MAURICIO;AYALA-RINC'N, MAURICIO2005 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.

36.
JACOBI, Ricardo P2005JACOBI, 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.

37.
KAMAREDDINE, Fairouz2004KAMAREDDINE, 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.

38.
M. Ayala-Rincón;AYALARINCON, M;Ayala-Rincon, M.;Ayala-Rincón, Mauricio;AYALA-RINCON, MAURICIO;AYALA-RINC´N, MAURICIO;AYALA-RINC'N, MAURICIO2003M. 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.

39.
M. Ayala-Rincón;AYALARINCON, M;Ayala-Rincon, M.;Ayala-Rincón, Mauricio;AYALA-RINCON, MAURICIO;AYALA-RINC´N, MAURICIO;AYALA-RINC'N, MAURICIO2003M. 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.

40.
M. Ayala-Rincón;AYALARINCON, M;Ayala-Rincon, M.;Ayala-Rincón, Mauricio;AYALA-RINCON, MAURICIO;AYALA-RINC´N, MAURICIO;AYALA-RINC'N, MAURICIO2003M. 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.

41.
M. Ayala-Rincón;AYALARINCON, M;Ayala-Rincon, M.;Ayala-Rincón, Mauricio;AYALA-RINCON, MAURICIO;AYALA-RINC´N, MAURICIO;AYALA-RINC'N, MAURICIO2002M. 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.

42.
M. Ayala-Rincón;AYALARINCON, M;Ayala-Rincon, M.;Ayala-Rincón, Mauricio;AYALA-RINCON, MAURICIO;AYALA-RINC´N, MAURICIO;AYALA-RINC'N, MAURICIO2002M. 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.

43.
MAYA NETO, R.2002M. 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.

44.
M. Ayala-Rincón;AYALARINCON, M;Ayala-Rincon, M.;Ayala-Rincón, Mauricio;AYALA-RINCON, MAURICIO;AYALA-RINC´N, MAURICIO;AYALA-RINC'N, MAURICIO2001M. 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.

45.
M. Ayala-Rincón;AYALARINCON, M;Ayala-Rincon, M.;Ayala-Rincón, Mauricio;AYALA-RINCON, MAURICIO;AYALA-RINC´N, MAURICIO;AYALA-RINC'N, MAURICIO2001 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.

46.
M. Ayala-Rincón;AYALARINCON, M;Ayala-Rincon, M.;Ayala-Rincón, Mauricio;AYALA-RINCON, MAURICIO;AYALA-RINC´N, MAURICIO;AYALA-RINC'N, MAURICIO2000M. Ayala-Rincón; Cesar Munoz . Explicit Substitutions and All That. Revista Colombiana de Computación, v. 1, n.1, p. 47-71, 2000.

47.
M. Ayala-Rincón;AYALARINCON, M;Ayala-Rincon, M.;Ayala-Rincón, Mauricio;AYALA-RINCON, MAURICIO;AYALA-RINC´N, MAURICIO;AYALA-RINC'N, MAURICIO1997 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.

48.
M. Ayala-Rincón;AYALARINCON, M;Ayala-Rincon, M.;Ayala-Rincón, Mauricio;AYALA-RINCON, MAURICIO;AYALA-RINC´N, MAURICIO;AYALA-RINC'N, MAURICIO1997M. 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.

49.
M. Ayala-Rincón;AYALARINCON, M;Ayala-Rincon, M.;Ayala-Rincón, Mauricio;AYALA-RINCON, MAURICIO;AYALA-RINC´N, MAURICIO;AYALA-RINC'N, MAURICIO1993M. 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.

Livros publicados/organizados ou edições
1.
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 .

2.
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 .

3.
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 .

4.
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 .

5.
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 .

6.
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 .

7.
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 .

8.
AYALARINCON, M; HAEUSLER, Edward Hermann (Org.) . Special Issue of The Logical Journal of the IGPL, Volume 17(5), Second Logical and Semantic Frameworks, with Applications - Guest Editor. Oxford: Oxford University Press, 2009. v. 17(5). 110p .

9.
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 .

10.
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 .

11.
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 .

12.
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 .

Capítulos de livros publicados
1.
Ramos, Thiago Mendonça Ferreira ; Muñoz, César ; Ayala-Rincón, Mauricio ; Moscato, Mariano ; Dutle, Aaron ; Narkawicz, Anthony . Formalization of the Undecidability of the Halting Problem for a Functional Language. In: Proc. Workshop on Logic, Language, Information and Computation WoLLIC 2018. (Org.). Lecture Notes in Computer Science. 1ed.: Springer Berlin Heidelberg, 2018, v. 10944, p. 196-209.

2.
Ayala-Rincón, Mauricio; de Carvalho-Segundo, Washington ; FERNÁNDEZ, MARIBEL ; NANTES-SOBRINHO, DANIELE . Nominal C-Unification. In: Logic-Based Program Synthesis and Transformation LOPSTR. (Org.). Lecture Notes in Computer Science. 1ed.: Springer International Publishing, 2018, v. 10855, p. 235-251.

3.
Ayala-Rincón, Mauricio; de Carvalho-Segundo, Washington ; FERNÁNDEZ, MARIBEL ; NANTES-SOBRINHO, DANIELE . On Solving Nominal Fixpoint Equations. In: LNAI Proc. Frontiers on Combining Systems FroCoS 2017. (Org.). Lecture Notes in Computer Science. 1ed.Heildelberg: Springer International Publishing, 2017, v. 10483, p. 209-226.

4.
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.

5.
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.

6.
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.

7.
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.

Trabalhos completos publicados em anais de congressos
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.

2.
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.

3.
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.

4.
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.

5.
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.

6.
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.

7.
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.

8.
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.

9.
Ayala-Rincon, M.; Carvalho Segundo, W.L.R. ; FERNANDEZ, M. ; NANTES-SOBRINHO, DANIELE . Nominal C-Unification. In: The 27th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2017), 2017, Namur. Pre-proceedings paper presented at the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2017), 2017. p. 1-16.

10.
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.

11.
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.

12.
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.

13.
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.

14.
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.

15.
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.

16.
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.

17.
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.

18.
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.

19.
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.

20.
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.

21.
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.

22.
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.

23.
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.

24.
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.

25.
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.

26.
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.

27.
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.

28.
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.

29.
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.

30.
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.

31.
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.

32.
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.

33.
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).

34.
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.

35.
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.

36.
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.

37.
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.

38.
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.

39.
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.

40.
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.

41.
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.

42.
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.

43.
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.

44.
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.

45.
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.

46.
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.

47.
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.

48.
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.

49.
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.

50.
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.

51.
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.

52.
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.

53.
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.

54.
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.

55.
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.

56.
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.

57.
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.

58.
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.

59.
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.

60.
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.

61.
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.

62.
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.

63.
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.

64.
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.

65.
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.

66.
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.

67.
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.

68.
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.

69.
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.

70.
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.

71.
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.

72.
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.

73.
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.

74.
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.

75.
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.

76.
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.

77.
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.

78.
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.

79.
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.

80.
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.

81.
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.

82.
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.

83.
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.

84.
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.

85.
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.

86.
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.

87.
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.

88.
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.

89.
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.

90.
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.

Resumos expandidos publicados em anais de congressos
1.
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.

2.
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.

3.
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.

4.
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.

5.
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.

6.
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.

Resumos publicados em anais de congressos
1.
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.

2.
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.

3.
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.

4.
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.

5.
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.

6.
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.

7.
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.

8.
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.

9.
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.

10.
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.

11.
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.

12.
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.

13.
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.

14.
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.

15.
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.

16.
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.

17.
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.

Resumos publicados em anais de congressos (artigos)
1.
M. Ayala-Rincón;AYALARINCON, M;Ayala-Rincon, M.;Ayala-Rincón, Mauricio;AYALA-RINCON, MAURICIO;AYALA-RINC´N, MAURICIO;AYALA-RINC'N, MAURICIO1996M. 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.

2.
M. Ayala-Rincón;AYALARINCON, M;Ayala-Rincon, M.;Ayala-Rincón, Mauricio;AYALA-RINCON, MAURICIO;AYALA-RINC´N, MAURICIO;AYALA-RINC'N, MAURICIO1996M. 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.

3.
M. Ayala-Rincón;AYALARINCON, M;Ayala-Rincon, M.;Ayala-Rincón, Mauricio;AYALA-RINCON, MAURICIO;AYALA-RINC´N, MAURICIO;AYALA-RINC'N, MAURICIO1996M. 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.

4.
M. Ayala-Rincón;AYALARINCON, M;Ayala-Rincon, M.;Ayala-Rincón, Mauricio;AYALA-RINCON, MAURICIO;AYALA-RINC´N, MAURICIO;AYALA-RINC'N, MAURICIO1994M. 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.

Artigos aceitos para publicação
1.
Soncco-Álvarez, J.L. ; MUNOZ, D. ; M. Ayala-Rincón . Opposition-Based Memetic Algorithm and Hybrid Approach for Sorting Permutations by Reversals. EVOLUTIONARY COMPUTATION, 2018.

Apresentações de Trabalho
1.
Ayala-Rincon, M.. Curso Intensivo (Universidad Nacional de Colombia - Manizales - 20h) Teoria de Prova. 2018. (Apresentação de Trabalho/Outra).

2.
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).

3.
Ayala-Rincon, M.. Palestra (Universidad Nacional de Colombia - Manizales) Terminación de Especificaciones Funcionales. 2017. (Apresentação de Trabalho/Conferência ou palestra).

4.
Ayala-Rincon, M.. Curso Intensivo (Universidad Nacional de Colombia - Manizales - 30h) Lógica Matemática. 2017. (Apresentação de Trabalho/Outra).

5.
Ayala-Rincon, M.. Invited talk (WEITC, IC UFF): Treating the undecidable - the case of termination. 2017. (Apresentação de Trabalho/Congresso).

6.
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).

7.
Ayala-Rincón, Mauricio. Palestra (UFG-IME) Statically Checking Termination. 2017. (Apresentação de Trabalho/Conferência ou palestra).

8.
M. Ayala-Rincón. Invited talk (UNEMAT 2016): Mechanical Formalization of Computational Properties. 2016. (Apresentação de Trabalho/Conferência ou palestra).

9.
Ayala-Rincon, M.. Talk (IFIP WG 1.6 Term Rewriting - Annual Meeting): Formalisation of Confluence. 2016. (Apresentação de Trabalho/Conferência ou palestra).

10.
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).

11.
M. Ayala-Rincón. Palestra (Universidad del Valle) Verification of Termination and Totality. 2016. (Apresentação de Trabalho/Conferência ou palestra).

12.
M. Ayala-Rincón. Invited Talk (DCM 2015): Formalising Confluence. 2015. (Apresentação de Trabalho/Conferência ou palestra).

13.
Ayala-Rincón, Mauricio. Palestra (Escuela Colombiana de Ingeniería): Formalising Confluence. 2015. (Apresentação de Trabalho/Conferência ou palestra).

14.
Ayala-Rincón, Mauricio. Invited short course (Nat@Logic, 4h): Formal Reasoning with PVS. 2015. (Apresentação de Trabalho/Conferência ou palestra).

15.
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).

16.
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).

17.
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).

18.
Ayala-Rincón, Mauricio. Invited short course (8CCC, 6h): Computational Deduction and Formal Proofs. 2013. (Apresentação de Trabalho/Conferência ou palestra).

19.
Ayala-Rincón, Mauricio. Invited talk (LACREST 2012): Formalising and Reusing of Proofs. 2012. (Apresentação de Trabalho/Conferência ou palestra).

20.
Ayala-Rincón, Mauricio. Palestra (UNQuilmes): Complexity and Algorithms for Sorting Sequences. 2012. (Apresentação de Trabalho/Conferência ou palestra).

21.
Ayala-Rincón, Mauricio. Palestra (UNQuilmes): Formalising and Reusing of Proofs. 2012. (Apresentação de Trabalho/Conferência ou palestra).

22.
Ayala-Rincón, Mauricio. Conferência convidada (IV SIMMI): Formalisation and Reusing of Proofs. 2012. (Apresentação de Trabalho/Conferência ou palestra).

23.
Ayala-Rincón, Mauricio. Invited talk (6CCC): Formal methods - On automating Termination. 2011. (Apresentação de Trabalho/Conferência ou palestra).

24.
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).

25.
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).

26.
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).

27.
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).

28.
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).

29.
Ayala-Rincón, Mauricio. Invited talk: Rewriting, Types, Proofs and Verified Sotware and Hardware. 2009. (Apresentação de Trabalho/Conferência ou palestra).

30.
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).

31.
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).

32.
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).

33.
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).

34.
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).

35.
Ayala-Rincón, Mauricio. Palestra (UFG): Especificação e Verificação de Sistemas Computacionais. 2007. (Apresentação de Trabalho/Conferência ou palestra).

36.
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).

37.
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).

38.
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).

39.
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).

40.
Ayala-Rincón, Mauricio. Palestra (Université de Bretagne Occidentale): Exploring Hardware via Rewriting Logic. 2003. (Apresentação de Trabalho/Conferência ou palestra).

41.
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).

42.
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).

Outras produções bibliográficas
1.
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).

2.
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).

3.
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).

4.
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).

5.
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).

6.
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).


Produção técnica
Assessoria e consultoria
1.
Ayala-Rincon, M.. Membro do comitê avaliador da segunda etapa do Edital 12/2017 Startups da FAPDF. 2018.

2.
M. Ayala-Rincón. Membro do Comitê de priorização de projetos do Edital 04/2017 ? Demanda Espontânea da FPDF. 2017.

3.
M. Ayala-Rincón. Membro do Comitê de priorização de projetos dos Programas COFECUB e PROBRAL. 2016.

4.
M. Ayala-Rincón. Membro do Comitê Julgador 1a rodada Edital MCT/SETEC/CNPq Nº 054/2013 ? RHAE Pesquisador na Empresa. 2014.

5.
Ayala-Rincón, Mauricio. Membro do Comitê de Seleção de Bolsistas Doutorado e Sandúiche DAAD/CNPq-CAPES. 2014.

6.
Ayala-Rincón, Mauricio. Membro do Comitê Julgador 2a rodada Edital MCT/SETEC/CNPq Nº 054/2013 ? RHAE Pesquisador na Empresa. 2014.

7.
M. Ayala-Rincón. Membro do Comitê de Seleção de Bolsistas Doutorado e Sandúiche DAAD/CNPq-CAPES. 2013.

8.
Ayala-Rincón, Mauricio. Membro do Comitê Técnico de Avaliação Propostas PAPPE Integração, Edital FAPDF 08. 2013.

9.
M. Ayala-Rincón. Membro do Comitê Julgador 1a rodada Edital MCT/SETEC/CNPq Nº 017/2012 ? RHAE Pesquisador na Empresa. 2012.

10.
Ayala-Rincon, M.. Membro do Comitê de Seleção de Bolsistas Doutorado e Sandúiche DAAD/CNPq-CAPES. 2012.

11.
Ayala-Rincon, M.. Membro do Comitê Julgador 1a rodada Edital MCT/SETEC/CNPq Nº 075/2010 ? RHAE Pesquisador na Empresa. 2011.

12.
Ayala-Rincón, Mauricio. Membro do Comitê de Seleção de Bolsistas Doutorado e Sandúiche DAAD/CNPq-CAPES. 2011.

13.
Ayala-Rincon, M.. Membro do Comitê Julgador 2a rodada Edital MCT/SETEC/CNPq Nº 075/2010 ? RHAE Pesquisador na Empresa. 2011.

14.
Ayala-Rincon, M.. Membro do Comitê Julgador 3a rodada Edital MCT/SETEC/CNPq Nº 075/2010 ? RHAE Pesquisador na Empresa. 2011.

15.
Ayala-Rincon, M.. Membro do Comitê Julgador do Prêmio Pesquisador do DF. 2011.

16.
Ayala-Rincon, M.. Membro do Comitê Julgador 1a rodada Edital MCT/SETEC/CNPq Nº 062/2009 ? RHAE Pesquisador na Empresa. 2010.

17.
Ayala-Rincon, M.. Membro do Comitê Julgador 2a rodada Edital MCT/SETEC/CNPq Nº 062/2009 ? RHAE Pesquisador na Empresa. 2010.

18.
Ayala-Rincon, M.. Membro do Comitê Julgador 3a rodada Edital MCT/SETEC/CNPq Nº 062/2009 ? RHAE Pesquisador na Empresa. 2010.

19.
AYALARINCON, M. Membro do Comitê Julgador 1a Rodada do Edital MCT/SETEC/CNPq nº 67/2008 - RHAE Pesquisador na Empresa. 2009.

20.
AYALARINCON, M. Membro do Comitê de Seleção de bolsistas DAAD/CNPq/CAPES. 2009.

21.
Ayala-Rincón, Mauricio. Membro do Comitê Julgador 2a Rodada do Edital MCT/SETEC/CNPq nº 67/2008 - RHAE Pesquisador na Empresa. 2009.

22.
Ayala-Rincón, Mauricio. Membro do Comitê Julgador 3a Rodada do Edital MCT/SETEC/CNPq nº 67/2008 - RHAE Pesquisador na Empresa. 2009.

23.
Ayala-Rincón, Mauricio. Consultor ad hoc em Ciência da Computação Edital PRONEX MCT/CNPq/FAPERGS 008/2009. 2009.

24.
AYALARINCON, M. Membro do Comitê Julgador, Edital MCT/CNPq/CT-Amazônia Nº 055/2008 - CT-Amazônia. 2008.

25.
AYALARINCON, M. Membro do Comitê Julgador 1a Rodada do Edital MCT/SETEC/CNPq nº 32/2007 - RHAE Pesquisador na Empresa. 2008.

26.
AYALARINCON, M. Membro do Comitê Julgador, 2a Rodada do Edital MCT/SETEC/CNPq nº 32/2007 - RHAE Pesquisador na Empresa. 2008.

27.
AYALARINCON, M. Membro do Comitê Julgador PROBRAL (CAPES/DAAD) edital 2006. 2006.

Programas de computador sem registro
1.
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.

2.
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.

3.
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.

4.
Ayala-Rincon, M.; Cesar Munoz ; Goodloe, Alwyn . Terminação pelo "size-change principle" via grafos de contextos de chamados em PVS. 2010.

5.
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.

6.
GALDINO, André Luiz ; AYALARINCON, M . TRS - PVS theory for term rewriting systems - Parte de NASA LaRC PVS library. 2008.

7.
GALDINO, André Luiz ; AYALARINCON, M . ARS - PVS theory for abstract reduction systems - Parte de NASA LaRC PVS library. 2007.

8.
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.

9.
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.

10.
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.

11.
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.

12.
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.

13.
M. Ayala-Rincón; L. M. R. Gadelha . Algoritmo de decisão para a aritmética de Presburger. 1995.

Trabalhos técnicos


Patentes e registros



Programa de computador
1.
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.
Patente: Programa de Computador. Número do registro: PI08031355, título: "Sistema de Controle Distribuído de Grupo de Elevadores Usando Dispositivos Reconfiguráveis" , Instituição de registro: INPI - Instituto Nacional da Propriedade Industrial.



Bancas



Participação em bancas de trabalhos de conclusão
Mestrado
1.
NANTES-SOBRINHO, DANIELE; HAEUSLER, Edward Hermann; Ayala-Rincón, Mauricio. Participação em banca de Bruno de Assis Delboni. Unificação Assimétrica Módulo Operadores Nilpotentes com Homomorfismo. 2017. Dissertação (Mestrado em Matemática) - Universidade de Brasília.

2.
Weigang, Li; Ladeira, Marcelo; Cozman, Fabio Gagliardi; Carvalho, Rommel Novaes; M. Ayala-Rincón. Participação em banca de Laécio Lima dos Santos. 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.

3.
ALVES, V. R.; Ayala-Rincón, Mauricio; TEIXEIRA, L. M.; MOTA, A. C.. Participação em banca de Thiago Mael de Castro. Commuting Strategies for Product-Line Reliability Analysis. 2016. Dissertação (Mestrado em Informática) - Universidade de Brasília.

4.
Weigang, Li; de Almeida Jr., Jorge Rady; Ayala-Rincón, Mauricio. Participação em banca de Lucas Borges Monteiro. 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.

5.
Aranha, Diego de Freitas; van de Graff, Jeroen; Ayala-Rincón, Mauricio. Participação em banca de Amanda Cristina Davi Resende. 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.

6.
MOURA, Flávio Leonardo Cavalcanti de; VENTURA, Daniel Lima; Ayala-Rincon, M.. Participação em banca de João Paulo Carvalho Colu de Queiroz. Um Estudo sobre Verificação Formal de Sistemas Concorrentes. 2012. Dissertação (Mestrado em Informática) - Universidade de Brasília.

7.
ALVES, V. R.; Ayala-Rincón, Mauricio; ALVES, C. F.; GHEYI, R.. Participação em banca de Giselle Barbosa Gomes Machado. 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.

8.
PIMENTEL, E.; VERGARA, C. R. G.; RODRIGUES FILHO, A. A.; Ayala-Rincón, Mauricio. Participação em banca de Wesley Luiz Alves da Mata. Sobre as lógicas linear, intuicionista e clássica e suas especi ficações. 2011. Dissertação (Mestrado em Matemática) - Universidade Federal de Minas Gerais.

9.
MOURA, Flávio Leonardo Cavalcanti de; BENEVIDES, M.; Ayala-Rincón, Mauricio. Participação em banca de Washington Luis Ribeiro de Carvalho Segundo. Verificação de Propriedades do Cálculo Lambda ex em Coq. 2010. Dissertação (Mestrado em Informática) - Universidade de Brasília.

10.
MOURA, Flávio Leonardo Cavalcanti de; Ayala-Rincón, Mauricio; RODRIGUES, P. H. A.. Participação em banca de Flávio José Ferro Barros. 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.

11.
M. Ayala-Rincón; LLANOS, Carlos; VIDAL FILHO, Walter de Brito. Participação em banca de Marcos Martins Melo. 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.

12.
M. Ayala-Rincón; MEIDANIS, João; WALTER, Maria Emilia Machado Telles. Participação em banca de Hederson Pereira dos Santos. Ordenação por Transposição baseado no Formalismo Algébrico. 2006. Dissertação (Mestrado em Mestrado Em Informática) - Universidade de Brasília.

13.
M. Ayala-Rincón; SAMPAIO, Marcus Costa; SAUVÉ, Jacques Philippe. Participação em banca de Hilmer Rodrigues Neri. 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.

14.
M. Ayala-Rincón; MATTOS, Luiz Antonio da Frota; FERNANDES, Clovis Torres. Participação em banca de Rodrigo de Almeida Sodré. Infraestrutura Formal de Segurança para Sistemas Distribuídos. 2001. Dissertação (Mestrado em Ciência da Computação) - Universidade de Brasília.

15.
M. Ayala-Rincón; JARDIM, Maria Helena Cautiero Horta; MAKLER, Susana Schleimberg de. Participação em banca de Rosângela de Fátima Sviercoski Ferreira. Uma Extensão do Algoritmo Proximal para Programação Linear Quadrática Estendida. 1996. Dissertação (Mestrado em Matemática) - Universidade de Brasília.

Teses de doutorado
1.
HAEUSLER, Edward Hermann; Dowek, G.; Ayala-Rincón, Mauricio; BENEVIDES, M.; Vieira, Bruno L.; PEREIRA, Luiz Carlos P D; Laber, Eduardo Sany. Participação em banca de Jeferson de Barros Santos. 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.

2.
TELLES, G. P.; GOG, S.; Laber, Eduardo Sany; M. Ayala-Rincón; Sadike Adi, S.; PEDROSA, L. L. C.. Participação em banca de Felipe Alves da Louza. Engineering Augmented Suffix Sorting Algorithms. 2017. Tese (Doutorado em Ciência da Computação) - Universidade Estadual de Campinas.

3.
QUEIROZ, R. G.; HAEUSLER, Edward Herman; MOURA, Flávio Leonardo Cavalcanti de; Bacelar, José Carlos; FREITAS, F. L. G.; Ayala-Rincón, Mauricio. Participação em banca de Marcus Vinicius Midena Ramos. Formalization of Context-Free Language Theory. 2016. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.

4.
PIMENTEL, E.; Rueda, Camilo; Ortiz Rico, Guillermo; Ayala-Rincón, Mauricio. Participação em banca de Carlos Ernesto Ramírez Ovalle. Sobre Extensiones Semánticas y Generalizaciones de Tipos en Lógica Lineal con Subexponenciales. 2016. Tese (Doutorado em Matemáticas) - Universidad Del Valle.

5.
Nascimento, A.; Renner, Renato; Broadbent, Anne; Roetteler, Martin; Ayala-Rincón, Mauricio. Participação em banca de Felipe Gomes Lacerda. Classical leakage-resilent circuits from quantum fault-tolerant computation. 2015. Tese (Doutorado em Informática) - Universidade de Brasília.

6.
WELLS, J. B.; KAMAREDDINE, Fairouz; Ayala-Rincón, Mauricio; MICHAELSON, G.. Participação em banca de John Pirie. 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.

7.
BONELLI, E.; RÍOS, Alejandro; KESNER, Delia; Aguirre, Nazareno; Miquel, Alexandre; Ayala-Rincón, Mauricio. Participação em banca de Carlos Lombardi. Reduction spaces in non-sequential and infinitary rewriting systems. 2014. Tese (Doutorado em L'UFR d'informatique - Lab. PPS) - Université Paris Diderot.

8.
HAEUSLER, Edward Hermann; Gordeev, Lew; Grisi de Oliveira, Anjolina; Ayala-Rincón, Mauricio; PEREIRA, Luiz Carlos P D; Casanova, Marco Antonio; BENEVIDES, M.. Participação em banca de Marcela Quispe Cruz. Some Results in a Proof-theory Based on Graphs. 2014. Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro.

9.
Bonelli, Eduardo; CONIGLIO, Marcelo Esteban; Areces, Carlos; Ayala-Rincón, Mauricio. Participação em banca de Gabriela Steren. 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.

10.
LLANOS, C. H.; Ayala-Rincón, Mauricio; HUEBNER, M.; CARVALHO, G. C.; BRAGA, A. P.. Participação em banca de André Luiz Sordi Braga. 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.

11.
QUEIROZ, R. G.; Scanlon, T.; Miraglia, F.; CONIGLIO, Marcelo Esteban; Ayala-Rincón, Mauricio. Participação em banca de Eudes Naziazeno Galvao. A Class of QFA Rings. 2011. Tese (Doutorado em Matemática) - Universidade Federal de Pernambuco.

12.
BECKER, Jürgen; HARTENSTEIN, Reiner W; Ayala-Rincón, Mauricio; Jondral, Friedrich; Siegel, Michael; Neumann, Cornelius. Participação em banca de Carlos Federico Morra. A Flexible Framework for Hardware/Software Design Space Exploration using Rewriting Logic. 2010. Tese (Doutorado em Elektrotechnik und Informationstechnik) - Karlsruher Institut für Technologie.

13.
HAEUSLER, Edward Hermann; M. Ayala-Rincón; Marcelo da Silva Corrêa; PEREIRA, Luiz Carlos P D; Geiza Maria Hamazaki Silva. Participação em banca de Vaston Gonçalves da Costa. Compactação de Provas Lógicas. 2007. Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro.

14.
RÍOS, Alejandro; M. Ayala-Rincón; KESNER, Delia; SZASZ, Nora. Participação em banca de Ariel Arbiser. Explicit Substitution: Systems and Subsystems. 2006. Tese (Doutorado em Ciencias de La Computación) - Universidad de Buenos Aires.

15.
HAEUSLER, Edward Herman; M. Ayala-Rincón; VELOSO, Paulo A S; PEREIRA, Luiz Carlos P D; CONIGLIO, Marcelo Esteban. Participação em banca de Geiza Maria Hamazaki Silva. Extração de programas de provas. 2004. Tese (Doutorado em Informática) - Pontifícia Universidade Católica do Rio de Janeiro.

Qualificações de Doutorado
1.
MUNOZ, D.; Teodoro, George; M. Ayala-Rincón. Participação em banca de Lucas Ângelo da Silveira. Algoritmos Bioinspirados Multi-ilhas para Problemas de Alta Complexidade. 2018. Exame de qualificação (Doutorando em Informática) - Universidade de Brasília.

2.
ROCCO, Noraí Romeu; VENTURA, Daniel Lima; Sobrinho, Daniele Nantes; M. Ayala-Rincón. Participação em banca de Nathália Nogueira Gonçalves. 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.

3.
SHUMYATSKY, Pavel; VENTURA, Daniel Lima; MOURA, Flávio Leonardo Cavalcanti de; M. Ayala-Rincón. Participação em banca de Sara Raissa Rodrigues. 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.

4.
SHUMYATSKY, Pavel; HAEUSLER, Edward Hermann; MOURA, Flávio Leonardo Cavalcanti de; M. Ayala-Rincón. Participação em banca de Gláucia Lenita Diering. 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.

5.
Sviridova, I.; HAEUSLER, Edward Hermann; MOURA, Flávio Leonardo Cavalcanti de; M. Ayala-Rincón. Participação em banca de John Freddy Moreno Lozada. 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.

6.
GARONZI, M.; HAEUSLER, Edward Hermann; NANTES-SOBRINHO, DANIELE; M. Ayala-Rincón. Participação em banca de Michell Lucena Dias. 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.

7.
TELLES, G. P.; WALTER, Maria Emilia Machado Telles; Teodoro, George; M. Ayala-Rincón. Participação em banca de Daniel Saad Nogueira Nunes. Dinamização de Estruturas de Dados Sucintas. 2016. Exame de qualificação (Doutorando em Informática) - Universidade de Brasília.

8.
M. Ayala-Rincón; HAEUSLER, Edward Hermann; ALVES, V. R.; MOURA, Flávio Leonardo Cavalcanti de. Participação em banca de Washington Luis Ribeiro de Carvalho Segundo. 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.

9.
SHUMYATSKY, Pavel; Ayala-Rincón, Mauricio; HAEUSLER, Edward Herman; MOURA, Flávio Leonardo Cavalcanti de. Participação em banca de Danilo Sanção da Silveira. 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.

10.
HAEUSLER, Edward Herman; ALVES, V. R.; MOURA, Flávio Leonardo Cavalcanti de; M. Ayala-Rincón. Participação em banca de Ariane Alves Almeida. Formalização da Equivalência entre Critérios de Terminação. 2016. Exame de qualificação (Doutorando em Informática) - Universidade de Brasília.

11.
SHUMYATSKY, Pavel; HAEUSLER, Edward Hermann; MOURA, Flávio Leonardo Cavalcanti de; M. Ayala-Rincón. Participação em banca de Danilo Sanção da Silveira. 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.

12.
ROCCO, Noraí Romeu; BENEVIDES, M.; MOURA, Flávio Leonardo Cavalcanti de; Ayala-Rincón, Mauricio. Participação em banca de Juliana Silva Canella. 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.

13.
TELLES, G. P.; Drummond, André; Brígido, Marcelo; M. Ayala-Rincón; Teodoro, George. Participação em banca de José Luis Soncco Álvarez. 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.

14.
QUEIROZ, R. G.; Ayala-Rincón, Mauricio; MOURA, Flávio Leonardo Cavalcanti de; FREITAS, F. L. G.. Participação em banca de Marcus Vinícius Midena Ramos. Language and Automata Theory Formalization. 2014. Exame de qualificação (Doutorando em Ciências da Computação) - Universidade Federal de Pernambuco.

15.
HAEUSLER, Edward Herman; ALVES, V. R.; MOURA, Flávio Leonardo Cavalcanti de; Ayala-Rincón, Mauricio. Participação em banca de Ana Cristina Rocha Oliveira Valverde. Formalização de Reescrita Nominal em PVS. 2014. Exame de qualificação (Doutorando em Informática) - Universidade de Brasília.

16.
SHUMYATSKY, Pavel; HAEUSLER, Edward Herman; MOURA, Flávio Leonardo Cavalcanti de; Ayala-Rincón, Mauricio. Participação em banca de Yerko Contreras Rojas. Teoria da Computação: teoria de reescrita e lógica formal. 2014. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.

17.
ZALESSKI, Pavel; HAEUSLER, Edward Herman; MOURA, Flávio Leonardo Cavalcanti de; Ayala-Rincón, Mauricio. Participação em banca de Jhoel Estebany Sandoval Gutierrez. Teoria da Computação: teoria de reescrita e lógica formal. 2014. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.

18.
ROCCO, Noraí Romeu; BENEVIDES, M.; MOURA, Flávio Leonardo Cavalcanti de; Ayala-Rincón, Mauricio. Participação em banca de Juliana Silva Canella. Teoria da Computação: teoria de reescrita e lógica formal. 2014. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.

19.
Godinho, Hemar T.; BENEVIDES, M.; MOURA, Flávio Leonardo Cavalcanti de; Ayala-Rincón, Mauricio. Participação em banca de Lucimeire Alves de Carvalho. Teoria da Computação: teoria de reescrita e lógica formal. 2014. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.

20.
KRASSALNIKOV, Alexei; HAEUSLER, Edward Hermann; MOURA, Flávio Leonardo Cavalcanti de; Ayala-Rincón, Mauricio; PETROGRADSKIY, V.; BRANDAO JUNIOR, A. P.. Participação em banca de Bruno Trinidade Reis. Qualificação em Teoria da Computação e Álgebra. 2013. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.

21.
LLANOS, C. H.; JACOBI, Ricardo P; Ayala-Rincón, Mauricio; Coelho Abade, Gustavo. Participação em banca de Janier Arias García. 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.

22.
Ayala-Rincón, Mauricio; HAEUSLER, Edward Hermann; MOURA, Flávio Leonardo Cavalcanti de; SHUMYATSKY, Pavel; ZALESSKI, Pavel; PINTO, A. G. S.. Participação em banca de Andréia Borges Avelar. Qualificação em Teoria da Computação e Álgebra. 2011. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.

23.
Ayala-Rincón, Mauricio; Nascimento, A.; HAEUSLER, Edward Hermann; PINTO, A. G. S.; SHUMYATSKY, Pavel; ZALESSKI, Pavel. Participação em banca de Thaynara Arielly Lima. Qualificação em Teoria da Computação e Álgebra. 2011. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.

24.
Ayala-Rincon, M.; FINGER, Marcelo; Nascimento, A.; ZALESSKI, Pavel; KRASSALNIKOV, Alexei; PINTO, A. G. S.. Participação em banca de Daniele Nantes Sobrinho. Teoria de Reescrita, Teoria de Prova e Criptografia. 2010. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.

25.
KRASSALNIKOV, Alexei; Ayala-Rincón, Mauricio; SHUMYATSKY, Pavel; HAEUSLER, Edward Hermann; MOURA, Flávio Leonardo Cavalcanti de; VIEIRA, A. C.. Participação em banca de Jorge Augusto Gonçalo de Brito. Qualificação em Álgebra e Teoria da Computação. 2009. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.

26.
HAEUSLER, Edward Hermann; MOURA, Flávio Leonardo Cavalcanti de; M. Ayala-Rincón; ZALESSKI, Pavel; SHUMYATSKY, Pavel; SIDKI, Said. Participação em banca de Vagner Rodrigues de Bessa. Qualificação em Álgebra e Teoria da Computação. 2008. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.

27.
HAEUSLER, Edward Hermann; MOURA, Flávio Leonardo Cavalcanti de; M. Ayala-Rincón; SHUMYATSKY, Pavel; SIDKI, Said; ZALESSKI, Pavel. Participação em banca de Flávia Ferreira Ramos. Qualificação em Álgebra e Teoria da Computação. 2008. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.

28.
SHUMYATSKY, Pavel; ZALESSKI, Pavel; FUTORNY, V.; MOURA, Flávio Leonardo Cavalcanti de; AYALARINCON, M; HAEUSLER, Edward Hermann. Participação em banca de Tonires Sales de Melo. Qualificação em Álgebra e Teoria da Computação. 2008. Exame de qualificação (Doutorando em Matemática) - Universidade de Brasília.

29.
M. Ayala-Rincón; KRASSALNIKOV, Alexei; SHUMYATSKY, Pavel; NALON, Cláudia; HAEUSLER, Edward Herman; ZALESSKI, Pavel. Participação em banca de Daniel Lima Ventura. 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.

30.
M. Ayala-Rincón; HAEUSLER, Edward Hermann; FINGER, Marcelo; SHUMYATSKY, Pavel; MAIER, Rudolf R; KRASSALNIKOV, Alexei. Participação em banca de André Luiz Galdino. 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.

31.
M. Ayala-Rincón; HAEUSLER, Edward Hermann; POUBEL, Haydée Werneck; MAIER, Rudolf R; ROCCO, Noraí Romeu; SHUMYATSKY, Pavel. Participação em banca de Flávio Leonardo Cavalcanti de Moura. 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.



Participação em bancas de comissões julgadoras
Concurso público
1.
WALTER, Maria Emilia Machado Telles; Ayala-Rincon, M.; TELLES, G. P.. Concurso para Professor Adjunto em Teoria de Computação. 2012. Universidade de Brasília.

2.
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.

3.
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.



Eventos



Participação em eventos, congressos, exposições e feiras
1.
8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP). PC member CPP 2019 - Afiliada a POPL. 2019. (Congresso).

2.
Co-chair 8th International Workshop on Confluence IWC 2019. co-chair Comitê de Programa do IWC 2009 (Jakob Grue Simonsen e M. Ayala-Rincón). 2019. (Congresso).

3.
IEEE Congress on Evolutionary Computation CEC 2019. Reviewer CeC 2019. 2019. (Congresso).

4.
International Conference on Formal Structures for Computation and Deduction. PC member FSCD 2019. 2019. (Congresso).

5.
13 Congreso Colombiano de Computación - 13CCC. PC member 13o Congreso Colombiano de Computación - 13CCC. 2018. (Congresso).

6.
13th Logical and Semantic Frameworks with Applications LSFA 2018. PC member 13th LSFA 2018. 2018. (Congresso).

7.
Co-chair 32nd International Workshop on Unification part of FLoC. PC chair UNIF 2018 - Colocado con FLoC 2018. 2018. (Congresso).

8.
IEEE Congress on Evolutionary Computing CeC 2018. PC Reviewer CeC 2018. 2018. (Congresso).

9.
Tenth NASA Formal Methods Symposium - NFM 2018. PC member Tenth NASA Formal Methods - NFM 2018. 2018. (Congresso).

10.
XLIV CLEI / SLTC Simpósio Latino-Americano em Teoria Computacional.PC member XLIV CLEI / SLTC. 2018. (Simpósio).

11.
12 Congreso Colombiano de Computación 12CCC. PC member 12o Congreso Colombiano de Computación - 12CCC. 2017. (Congresso).

12.
17th International Conference on Intelligent Systems Design and Applications (ISDA 2017). PC member ISDA 2017. 2017. (Congresso).

13.
Co-chair Eighth International Conference Interative Theorem Proving ITP 2017. PC co-chair 8th ITP 2017. 2017. (Congresso).

14.
Eleventh International Symposium on Frontiers of Combining Systems FroCoS 2017.PC member 11th FroCos 2017. 2017. (Simpósio).

15.
IEEE Congress on Evolutionary Computation CeC 2017. PC reviewer CeC 2017. 2017. (Congresso).

16.
Twelfth Logical and Semantic Frameworks with Applications- LSFA 2017. PC member 12th LSFA 2017. 2017. (Congresso).

17.
11 Congreso Colombiano de Computación - 11CCC. PC member 11o Congreso Colombiano de Computación - 11CCC. 2016. (Congresso).

18.
13th International Colloquium on Theoretical Aspects of Computing - ICTAC 2016. PC member 13th ICTAC 2016. 2016. (Congresso).

19.
16th International Conference on Intelligent Systems Design and Applications (ISDA). PC member 16th ISDA 2016. 2016. (Congresso).

20.
8th World Congress on Nature and Biologically Inspired Computing (NaBiC 2016 h. PC member 8th NaBIC 2016. 2016. (Congresso).

21.
Eleventh Logical and Semantic Frameworks with Applications- LSFA 2016. PC member 11th LSFA 2016. 2016. (Congresso).

22.
IEEE Congress on Evolutionary Computation CeC 2016. PC reviewer CeC 2016. 2016. (Congresso).

23.
12th International Colloquium on Theoretical Aspects of Computing - ICTAC 2015. PC member 12th ICTAC 2015. 2015. (Congresso).

24.
26th International Conference on Rewriting Techniques and Applications RTA 2015. PC member 26th RTA 2015. 2015. (Congresso).

25.
28th Symposium on Integrated Circuits and Systems Design - SBCCI 2015. PC member 28th SBCCI. 2015. (Congresso).

26.
4th International Workshop on Confluence - IWC 2015. PC member IWC 2015. 2015. (Congresso).

27.
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).

28.
Décimo Congreso Colombiano de Computación - 10CCC. Membro do Comitê Científico do Décimo Congreso Colombiano de Computación - 10CCC. 2015. (Congresso).

29.
Developments in Computational Models DCM 2015 / ICTAC 2015. Invited talk: Formalising Confluence. 2015. (Congresso).

30.
IEEE Congress on Evolutionary Computation CeC 2015. PC reviewer CeC 2015. 2015. (Congresso).

31.
International Joint Conference on Artificial Intelligence (IJCAI'15). Senior PC member IJCAI 2015. 2015. (Congresso).

32.
Nat@Logic - TRS School on Reasoning.Invited Lecturer - Formal Reasoning with PVS - 4h short-course. 2015. (Oficina).

33.
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).

34.
14th International Conference on Intelligent Systems Design and Applications (ISDA). PC member 14th International Conference on Intelligent Systems Design and Applications (ISDA). 2014. (Congresso).

35.
17th Brazilian Logic Conference (EBL 2014). PC member 17th EBL. 2014. (Congresso).

36.
23rd International Workshop on Functional and (Constraint) Logic Programming WFLP. PC member 23rd International Workshop on Functional and (Constraint) Logic Programming - WFLP. 2014. (Congresso).

37.
27th Symposium on Integrated Circuits and Systems Design - SBCCI 2014.PC member 27th SBCCI. 2014. (Simpósio).

38.
4th World Congress on Information and Communication Technologies WCIT 2014. PC member 4th World Congress on Information and Communication Technologies. 2014. (Congresso).

39.
6th World Congress on Nature and Biologically Inspired Computing (NaBiC 2014. PC member 6th World Congress on Nature and Biologically Inspired Computing. 2014. (Congresso).

40.
7th International School on Rewriting (ISR 2014). Invited Lecturer - Formalisation in PVS of Rewriting Properties - 6h Mini-course. 2014. (Congresso).

41.
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).

42.
Concurso de Teses e Dissertações - CTD 2014 (Congresso da SBC 2014). Miembro do Comitê Avaliador CTD-SBC 2014. 2014. (Congresso).

43.
IEEE Congress on Evolutionary Computation CeC 2014. PC reviewer CeC 2014. 2014. (Congresso).

44.
IX Southern Programmable Logic Conference SPL. Membro do Comitê Científico do SPL2014. 2014. (Congresso).

45.
Noveno Congreso Colombiano de Computación - 9CCC. Membro do Comitê Científico do Noveno Congreso Colombiano de Computación - 9CCC. 2014. (Congresso).

46.
PhD forum - IEEE CS Annual Symposium on VLSI. Membro do Comitê Julgador do PhD forum do 2014 ISVLSI. 2014. (Congresso).

47.
The Fifth International Symposium on Innovations in Information & Communications Technology (ISIICT 2014). PC member ISIICT 2014. 2014. (Congresso).

48.
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).

49.
26th Symposium on Integrated Circuits and Systems Design - SBCCI 2013.PC member 26th SBCCI. 2013. (Simpósio).

50.
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).

51.
5th World Congress on Nature and Biologically Inspired Computing (NaBiC 2013). PC member 5th World Congress on Nature and Biologically Inspired Computing. 2013. (Congresso).

52.
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).

53.
Eighth Logical and Semantic Frameworks, with Applications - LSFA 2013.Membro do Comitê Científico do 8th LSFA. 2013. (Simpósio).

54.
IEEE Congress on Evolutionary Computation CeC 2013. PC reviewer CeC 2013. 2013. (Congresso).

55.
PhD forum - IEEE CS Annual Symposium on VLSI. Membro do Comitê Julgador do PhD forum do 2013 ISVLSI. 2013. (Congresso).

56.
2012 7th Colombian Computing Congress (7CCC). Membro do Comitê Científico do Séptimo Congreso Colombiano de Computación - 7CCC. 2012. (Congresso).

57.
25th Symposium on Integrated Circuits and Systems Design - SBCCI 2012.PC member 25th SBCCI. 2012. (Simpósio).

58.
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).

59.
IEEE Congress on Evolutionary Computation CeC 2012. PC reviewer CeC 2012. 2012. (Congresso).

60.
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).

61.
IV Simpósio de Matemática Industrial SIMMI.Palestra convidada: Reuso de Demonstrações Formais em PVS. 2012. (Simpósio).

62.
Latin American Congress on Requirements Engineerings & Software Testing LACREST. Palestra convidada: Reusing Formal Proofs Through Isomorophisms. 2012. (Congresso).

63.
PhD forum - IEEE CS Annual Symposium on VLSI. Membro do Comitê Julgador do PhD forum do 2012 ISVLSI. 2012. (Congresso).

64.
Seventh Logical and Semantic Frameworks, with Applications - LSFA 2012.Membro do Comitê Científico do 7th LSFA. 2012. (Simpósio).

65.
VIII Southern Programable Logic Conference SPL. Membro do Comitê Científico. 2012. (Congresso).

66.
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).

67.
21st International Conference on Field Programable Logic and Applications FPL 2011. Membro do Comitê Científico. 2011. (Congresso).

68.
24rd Symposium on Integrated Circuits and Systems Design - SBCCI 2011.Membro do Comitê do Programa SBCCI 2011. 2011. (Simpósio).

69.
PhD forum IEEE CS annual Symposium on VLSI.Membro do Comitê do Programa do ISVLSI 2010 PhD Forum. 2011. (Simpósio).

70.
Sixth Logical and Semantic Frameworks, with Applications - LSFA 2011.Membro do Comitê do Programa LSFA 2011. 2011. (Simpósio).

71.
20th International Conference on Field Programable Logic and Applications FPL 2010. Membro do Comitê Científico. 2010. (Congresso).

72.
23rd Symposium on Integrated Circuits and Systems Design - SBCCI 2010.Membro do Comitê de Programa SBCCI 2010. 2010. (Simpósio).

73.
Fifth Logical and Semantic Frameworks, with Applications - LSFA 2010. Membro do Comitê de Programa LSFA 2010. 2010. (Congresso).

74.
PhD forum IEEE CS annual Symposium on VLSI. Membro do Comitê de Programa PhD Forum ISVLSI 2010. 2010. (Congresso).

75.
Quinto Congreso Colombiano de Computación - 5CCC. Membro do Comitê de Programa V CCC 2010. 2010. (Congresso).

76.
Reconfigurable Communication-centric Systems on Chip - ReCoSoC 2010. Palestra convidada: Automatizing the verification of the termination property of algorithms and processes. 2010. (Congresso).

77.
SEMISH - XXXVII Seminário Integrado de Software e Hardware.Membro do Comitê de Programa SEMISH 2010. 2010. (Seminário).

78.
19th International Conference on Field Programmable Logic and Applications - FPL 2009. Membro do Comitê Científico. 2009. (Congresso).

79.
22nd Symposium on Integrated Circuits and Systems Design - SBCCI 2009.Membro do Comitê de Programa SBCCI 2009. 2009. (Simpósio).

80.
9th International Workshop on Reduction Strategies in Rewriting and Programming - WRS 2009. Membro do Comitê Científico do 9th WRS 2009. 2009. (Congresso).

81.
Co-chair Fourth Logical and Semantic Frameworks, with Applications - LSFA 2009. Co-chair Comitê de Programa do LSFA 2009. 2009. (Congresso).

82.
Cuarto Congreso Colombiano de Computación - 4CCC. Palestra convidada: Rewriting, Types, Proofs and Veri ed Software & Hardware. 2009. (Congresso).

83.
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).

84.
I Simpósio de Matemática Industrial SIMMI.Palestra convidada: Rewriting Theory, Type Theory, Proof Theory and Verification. 2009. (Simpósio).

85.
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).

86.
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).

87.
18th International Conference on Field Programmable Logic and Applications - FPL 2008. Membro do Comitê Científico. 2008. (Congresso).

88.
21st Symposium on Integrated Circuits and Systems Design - SBCCI 2008. Membro do Comitê de Programa SBCCI 2008. 2008. (Congresso).

89.
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).

90.
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).

91.
Third Wokrshop on Logical and Semantic Frameworks, with Applications - LSFA 2008. Membro do Comitê Científico. 2008. (Congresso).

92.
14th Reconfigurable Architectures Workshop RAW 2007. Membro do Comitê Científico. 2007. (Congresso).

93.
17th International Conference on Field Programmable Logic and Applications - FPL 2007. Membro do Comitê Científico. 2007. (Congresso).

94.
20th Symposium on Integrated Circuits and Systems Design - SBCCI 2007. Membro do Comitê Científico. 2007. (Congresso).

95.
Co-chair Second Wokrshop on Logical and Semantic Frameworks, with Applications - LSFA 2007. Co-chair Comitê de Programa do LSFA 2007. 2007. (Congresso).

96.
Regional Meeting on Reconfigurable Computing RMRC.Membro do Comitê de Programa, Regional Meeting on Reconfigurable Computing RMRC. 2007. (Encontro).

97.
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).

98.
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).

99.
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).

100.
XXXIII Conferencia Latinoamericana de Informática - CLEI 2007. Membro do Comitê Científico. 2007. (Congresso).

101.
19th Symposium on Integrated Circuits and Systems Design - SBCCI 2005. Membro do Comitê de Programa SBCCI 2006. 2006. (Congresso).

102.
Co-chair Wokrshop on Logical and Semantic Frameworks, with Applications - LSFA 2006. Co-chair Comitê de Programa do LSFA 2006. 2006. (Congresso).

103.
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).

104.
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).

105.
XXXI Conferencia Latinoamericana de Informática - CLEI 2005. Membro do Comitê de Programa CLEI 2005. 2005. (Congresso).

106.
Concurso de Teses e Dissertações - CTD 2004 (Congresso da SBC 2004).Membro do Comitê de Programa CDT/SBC 2004. 2004. (Outra).

107.
5th Latin American Symposium on Theoretical Informatic LATIN 2002. Membro do Comitê de Programa LATIN 2002. 2002. (Congresso).

108.
Thirty Five years of Automath. Membro do Comitê de Programa 35 years of Automath. 2002. (Congresso).

109.
Workshop on Logic, Language, Information and Computation - WoLLIC 2002. Membro do Comitê de Programa WoLLIC 2002. 2002. (Congresso).

110.
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).

111.
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).

112.
Festival Workshop in Foundations and Computations.Session Chair: Festival Workshop in Foundations and Computations. 2000. (Outra).


Organização de eventos, congressos, exposições e feiras
1.
M. Ayala-Rincón; KESNER, Delia . Steering Committee Member - International Conference on Formal Structures for Computation and Deduction FSCD 2019. 2018. (Congresso).

2.
Moser, G. ; Dowek, G. ; Stump, A. ; Rose, K. ; M. Ayala-Rincón ; Tison, Sophie . Steering Committee member - 25th International Conference on Rewriting Techiques and Applications -RTA 2014. 2015. (Congresso).

3.
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).

4.
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).

5.
Ayala-Rincón, Mauricio; Rose, K. ; Dowek, G. ; Stump, A. ; Tison, Sophie ; Hirokawa, Nao . Steering Committee member - 26th International Conference on Rewriting Techiques and Applications -RTA 2015. 2014. (Congresso).

6.
M. Ayala-Rincón; Moser, G. ; Lucas, Salvador ; Blanqui, Fréderic ; Tison, Sophie ; Sakai, Masahiko . Steering Committee member - 24th International Conference on Rewriting Techiques and Applications -RTA 2013. 2013. (Congresso).

7.
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).

8.
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).

9.
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).

10.
Ayala-Rincon, M.. Publication Chair - 25th Symposium on Integrated Circuits and Systems Design - SBCCI 2012. 2012. (Congresso).

11.
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).

12.
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).

13.
KIRCHNER, C. ; Middeldorp, Aart ; Ayala-Rincon, M. ; OOSTROM, V. V. . Steering Committee member - Fifth International School on Rewriting - ISR 2010. 2010. (Outro).

14.
TREINEN, R. ; CURIEN, P. ; M. Ayala-Rincón . Conference Chair - Federated Conference on Rewriting, Deduction, and Programming, RDP 2009. 2009. (Congresso).

15.
AYALARINCON, M; MOURA, Flávio Leonardo Cavalcanti de . Organising co-Chair - Fourth International School on Rewriting - ISR 2009. 2009. (Outro).

16.
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).

17.
Ayala-Rincon, M.; TREINEN, R. . OC chair - 20th International Conference on Rewriting Techiques and Applications -RTA 2009. 2009. (Congresso).

18.
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).

19.
QUEIROZ, R. G. ; KAMAREDDINE, Fairouz ; M. Ayala-Rincón ; HODGES, W. . OC member - Workshop on Logic, Language, Information and Computation - WoLLIC 2008. 2008. (Congresso).

20.
M. Ayala-Rincón; HAEUSLER, Edward Hermann . OC member - Second Wokrshop on Logical and Semantic Frameworks, with Applications - LSFA 2007. 2007. (Congresso).

21.
BRAGA, Christiano ; M. Ayala-Rincón ; HAEUSLER, Edward Hermann . OC co-chair - Wokrshop on Logical and Semantic Frameworks, with Applications - LSFA 2006. 2006. (Congresso).

22.
QUEIROZ, R. G. ; M. Ayala-Rincón ; HAEUSLER, Edward Hermann . OC Chair - Workshop on Logic, Language, Information and Computation - WoLLIC 2001. 2001. (Congresso).



Orientações



Orientações e supervisões em andamento
Dissertação de mestrado
1.
Mehwish Arshid. Tópicos em unificação por definir. Início: 2018. Dissertação (Mestrado em Informática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. (Orientador).

Tese de doutorado
1.
Bruno de Assis Delboni. Estudo de Problemas em Unificação Módulo TBD. Início: 2017. Tese (Doutorado em Matemática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. (Orientador).

2.
Thiago Mendonça Ferreira Ramos. Formalização da Terminação de Programas Funcionais Com Sistemas de Tipos Elaborados. Início: 2017. Tese (Doutorado em Informática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. (Orientador).

3.
Kaliana dos Santos Dias de Freitas. Problemas em Extensões do Cálculo Lambda. Início: 2017. Tese (Doutorado em Informática) - Universidade de Brasília. (Orientador).

4.
Lucas Angelo da Silveira. Paralelização de algoritmos genéticos para distância evolutiva. Início: 2016. Tese (Doutorado em Informática) - Universidade de Brasília. (Orientador).

5.
Daniel Saad Nogueira Nunes. Estruturas e algoritmos eficientes. Início: 2014. Tese (Doutorado em Informática) - Universidade de Brasília. (Orientador).

6.
Washington Luis Ribeiro de Carvalho Segundo. Análise e formalização de sistemas de tipos nominais. Início: 2014. Tese (Doutorado em Informática) - Universidade de Brasília. (Orientador).

7.
Ariane Alves Almeida. Formalização da Noção de Terminação por Pares Dependentes para Programas Funcionais. Início: 2014. Tese (Doutorado em Informática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. (Orientador).

Iniciação científica
1.
Nikson Bernardes Fernandes Ferreira. Formalização de algoritmos de ordenação com ordens abstractos sobre um tipo não interpretado. Início: 2018. Iniciação científica (Graduando em Engenharia Mecatrônica) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico. (Orientador).


Orientações e supervisões concluídas
Dissertação de mestrado
1.
Thiago Mendonça Ferreira Ramos. 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.

2.
Lucas Angelo da Silveira. 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.

3.
Ariane Alves Almeida. 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.

4.
Daniel Saad Nogueira Nunes. 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.

5.
José Luis Soncco Álvarez. 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.

6.
Ana Cristina Rocha Oliveira Valverde. 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.

7.
Fábio Henrique da Silva. 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.

8.
José Luiz Correa de Moraes. 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.

9.
Thaynara Arielly de Lima. 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.

10.
Andréia Borges Avelar. 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.

11.
Daniele Nantes Sobrinho. 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.

12.
Rodrigo Borges Nogueira. 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.

13.
Rodrigo César de Castro Miranda. 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.

14.
Daniel Lima Ventura. 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.

15.
Thomas Mailleux Santana. 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.

16.
Hélio Carneiro Ferreira. 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.

17.
Valnei Alves Fernandes. 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.

18.
Flávio Leonardo Cavalcanti de Moura. 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.

19.
Rinaldi Maya Neto. 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.

20.
Wellington Barros e Barbosa. 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.

21.
Alexsandro Fernandes da Fonseca. 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.

22.
Luiz Manoel Gadelha Junior. 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.

23.
Vaston Gonçalves da Costa. 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.

24.
Ivan Eid Tavares de Araújo. 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.

25.
Yukiko Massago. 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.

26.
Pablo Domingues Conejo. 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.

Tese de doutorado
1.
José Luis Soncco Álvarez. 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.

2.
Ana Cristina Rocha Oliveira Valverde. 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.

3.
Thaynara Arielly de Lima. 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.

4.
Andréia Borges Avelar. 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.

5.
Daniele Nantes Sobrinho. 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.

6.
Carlos Federico Morra. 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.

7.
Daniel Lima Ventura. 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.

8.
André Luiz Galdino. 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.

9.
Flávio Leonardo Cavalcanti de Moura. 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.

Supervisão de pós-doutorado
1.
Besiki Dundua. 2015. Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Mauricio Ayala Rincon.

2.
Daniele Nantes Sobrinho. 2014. Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. Mauricio Ayala Rincon.

3.
André Luiz Galdino. 2013. Universidade de Brasília, . Mauricio Ayala Rincon.

4.
Daniel Lima Ventura. 2011. Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Mauricio Ayala Rincon.

Trabalho de conclusão de curso de graduação
1.
Thiago Mendonça Ferreira Ramos. 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.

2.
Daniel Saad Nogueira Nunes. 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.

Iniciação científica
1.
Nikson Bernardes Fernandes Ferreira. Formalização da correção do algoritmo de Ford-Johnson. 2018. 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.

2.
Danylo Andriushchenko. 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.

3.
Jadiel Teófilo Amorim de Oliveira. 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.

4.
Andressa Teixeira Sales. 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.

5.
Lucas de Moura Amaral. 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.

6.
Jéssyca Cristine Lima de Souza. 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.

7.
Jéssyca Cristine Lima de Souza. 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.

8.
Thiago Mendonça Ferreira Ramos. 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.

9.
Aurora Li Min de Freitas Wang. 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.

10.
Yuri Santos Rego. 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.

11.
Jéssyca Cristine Lima de Souza. 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.

12.
Thiago Mendonça Ferreira Ramos. 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.

13.
Thiago Mendonça Ferreira Ramos. 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.

14.
Yuri Santos Rego. 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.

15.
Alexandre Andrade Amaral. 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.

16.
Thiago Mendonça Ferreira Ramos. 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.

17.
Ana Cristina Rocha Oliveira. 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.

18.
Yuri Santos Rego. 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.

19.
Ana Cristina Rocha Oliveira. 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.

20.
Fábio Salgado de Carvalho. 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.

21.
Rebecca Caldas Curley. 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.

22.
Ana Cristina Rocha Oliveira. 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.

23.
Fábio Henrique da Silva. 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.

24.
Fábio Henrique da Silva. 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.

25.
Marcelo Henrique de Oliveira. 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.

26.
Danilo Tocantins Rufo Costa. 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.

27.
Claudio Celso Soares de Oliveira. 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.

28.
Roberto Evelim Penha Borges. 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.

29.
Aline Cosme da Cunha. 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.

30.
Diogo Pereira Almeida. 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.

31.
Claudio Celso Soares de Oliveira. 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.

32.
Marrise Neves da Rocha. 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.

33.
Rodrigo Borges Nogueira. 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.

34.
Felipe Paulino Tavares. 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.

35.
Rodrigo Borges Nogueira. 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.

36.
Marcos de Andrade Gomes. 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.

37.
Hélio Carneiro Ferreira. 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.

38.
Fred Ulisses Maranhão. 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.

39.
Alison Hugo Rodrigues Silva. 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.

40.
Alison Hugo Rodrigues Silva. 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.

41.
Vander Ramos Alves. 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.

42.
Luiz Manoel Gadelha Junior. 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.

43.
André Elvas. 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.

44.
Luiz Manoel Gadelha Junior. 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.

45.
Luciano Carvalho. 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.

Orientações de outra natureza
1.
Gabriel Nóbrega Bufolo. 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.

2.
André Figueira Lourenço. 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.

3.
Yuri Cosic Lavinas. 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.

4.
Hélio Carneiro Ferreira. 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.



Inovação



Programa de computador registrado
1.
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.
Patente: Programa de Computador. Número do registro: PI08031355, título: "Sistema de Controle Distribuído de Grupo de Elevadores Usando Dispositivos Reconfiguráveis" , Instituição de registro: INPI - Instituto Nacional da Propriedade Industrial.


Programa de computador sem registro
1.
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.


Projetos de pesquisa


Educação e Popularização de C & T



Livros e capítulos
1.
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 .

2.
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 .

3.
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 .




Página gerada pelo Sistema Currículo Lattes em 19/11/2018 às 13:32:23