Rede de Colaboração
Diretório de grupos de pesquisa

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

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, membro do Corpo Editorial da Revista Colombiana de Computación, pesquisador e consultor ad-hoc do Conselho Nacional de Desenvolvimento Científico e Tecnológico - CNPq. Foi Pesquisador Associado (1999-2000), está atualmente afiliado ao Grupo ULTRA da Heriot-Watt University (Edimburgo, U.K.) e foi 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, lambda calculus, 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 de uma metodologia baseada em reescrita-lógica para o projeto de hardware reconfigurável. Eleito "Conference Chair" da "Federated Conference on Rewriting, Deduction and Programming - RDP 2009" realizada em Brasília em junho/julho de 2009. RDP incluiu as conferências "9th Typed Lambda Calculus and Applications" e "20th Rewriting Techniques and Applications".
(Texto informado pelo autor)

Última atualização do currículo em 01/02/2012
Endereço para acessar este CV:
http://lattes.cnpq.br/8466420403941522
Dados pessoais
NomeMauricio Ayala Rincon
Nome em citações bibliográficasM. Ayala-Rincón;AYALARINCON, M;Ayala-Rincon, M.;Ayala-Rincón, Mauricio
SexoMasculino
Endereço profissionalUniversidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática.
Departamento de Matemáticas, Universidade de Brasília Campus Universitário Darcy Ribeiro
Asa Norte
70900-010 - Brasilia, DF - Brasil
Telefone: (61) 33072442 Ramal: 210 Fax: (61) 32732737
URL da Homepage: www.mat.unb.br/~ayala

Formação acadêmica/Titulação
1999 - 2000Pós-Doutorado .
Heriot-Watt University.
Bolsista do(a): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior ,CAPES ,Brasil .
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação / Especialidade: Lógicas e Semântica de Programas.
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação / Especialidade: Computabilidade e Modelos de Computação.
1994 - 1994Pó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 / Área: Ciência da Computação / Subárea: Matemática da Computação.
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação.
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação / Especialidade: Análise de Algoritmos e Complexidade de Computação.
1989 - 1993Doutorado em Fachbereich Informatik .
Universitaet Kaiserslautern.
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 / Área: Ciência da Computação / Subárea: Teoria da Computação.
1981 - 1987Graduação em Matemática .
Universidad de Los Andes.
Título: Algunos Aspectos de la Teoria de Bifurcaciones.
Orientador: Prof Dr. rer. nat. Jaime Lesmes.
1980 - 1985Graduação em Ingeniería de Sistemas y Computación .
Universidad de Los Andes.
Título: Generador de Evaluadores para Gramáticas con Atributos Fuertemente No-Circulares.
Orientador: Prof Dr. Rodrigo Lopez.

Atuação profissional
Fundação de Amparo à Pesquisa do Estado da Bahia, FAPESB, Brasil.
Vínculo institucional
2011 - 2011 Vínculo: Colaborador, Enquadramento Funcional: Consultor, Carga horária: 2
Outras informações Consultor projetos em Ciência da Computação
KINGS COLLEGE, KCL, Inglaterra.
Vínculo institucional
2012 - 2012 Vínculo: Professor vistante, Enquadramento Funcional: Colaborador, 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: Colaborador, 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
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).
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
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.
Heriot-Watt University, HWU, Grã-Bretanha.
Vínculo institucional
2001 - Atual 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
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
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
09/2010 - AtualConselhos, 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.
05/2010 - AtualDireçã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.
2010 - AtualAtividades de Participação em Projeto, Instituto de Ciências Exatas / Programas de Pós Matemática e Informática, .
Projetos de pesquisa
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
2010 - AtualAtividades de Participação em Projeto, Instituto de Ciências Exatas / Programas de Pós Matemática e Informática, .
Projetos de pesquisa
Coordenador do projeto UNIVERSAL 481783/2010-5: Substituições Explícitas, Terminação, Formalização de Sistemas e Aplicações Computacionais
08/2009 - AtualEnsino, Ciência da Computação, Nível: Graduação.
Disciplinas ministradas
Lógica Computacional (2009 II, 2010 I, 2010 II, 2011 I, 2011 II)
1/2003 - AtualEnsino, Informática, Nível: Pós-Graduação.
Disciplinas ministradas
Projeto e Análise de Algoritmos 2 (11 II)
Tópicos em Fundamentos e Métodos da Computação: Teoria de Tipos (11 I)
Estágios de Pesquisa (05I,05II,06I,06II,07I,07II)
Projeto e Complexidade de Algoritmos (03I)
Seminário Vinculado (2010 I)
Teoria da Computação (03II,04II,05II,08II,10II, 11II)
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 de Computação: Análise de Algoritmos para Biocomputação (04I)
1/2001 - AtualAtividades de Participação em Projeto, Instituto de Ciências Exatas, Departamento de Matemática.
Projetos de pesquisa
Participação em projeto conjunto 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 do programa Auxílio Complementar à Pesquisa DPP/UnB e EPSR
01/1996 - AtualPesquisa e desenvolvimento , Instituto de Ciências Exatas, Departamento de Ciência da Computação.
Linhas de pesquisa
Aplicações da teoria de reescrita
Animação de algoritmos e visualização
Teoria de reescrita, reescrita-lógica e aplicações
Computação eficiente para processamento de seqüências
1/1995 - AtualPesquisa e desenvolvimento , Instituto de Ciências Exatas, Departamento de Matemática.
Linhas de pesquisa
Cálculo lambda e cálculos de substituições explícitas
Análise de Algoritmos
Dedução Automática baseada em técnicas de reescrita
Especificação Algébrica
Sistemas de Reescrita
Teoria dos Tipos
Substituições Explícitas
1/1995 - AtualEnsino, 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)
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)
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), Teoria de Reescrita Avançada (2007II, 2008II, 2009II)
Tópicos em Computação: Teoria de Tipos (02I,04II), Linguagens Formais e Autômatos II (2007I)
2012 - 2013Atividades de Participação em Projeto, Instituto de Ciências Exatas/Programa de Pós-Graduação em Inforrmática, .
Projetos de pesquisa
Coordenador do projeto de cooperação internacional STIC-AmSud Brasil/França/Argentina (CAPES/INRIA/MINCYT, Edital 2011), Desenvolvimento Formal de Programas e Aplicações - DeCoPA
06/2008 - 12/2010Atividades de Participação em Projeto, Instituto de Ciências Exatas / Programas de Pós Matemática e Informática, .
Projetos de pesquisa
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
02/2008 - 12/2010Atividades de Participação em Projeto, Instituto de Ciências Exatas / Programas de Pós Matemática e Informática, .
Projetos de pesquisa
Coordenador do projeto FAPDF 8-004/2007, Verificação Formal de Protocolos de Comunicação com Aplicações em Criptografia
2008 - 2010Atividades de Participação em Projeto, Instituto de Ciências Exatas / Programas de Pós Matemática e Informática, .
Projetos de pesquisa
Participação em Projeto PROBRAL (CAPES/DAAD), Processo 304/08, Formally Designed Reconfigurable Architectures for High Performance Applications
1/1995 - 7/2009Ensino, 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/2009Conselhos, 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/2007Direçã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).
1/2005 - 7/2007Atividades de Participação em Projeto, Instituto de Ciências Exatas, Departamentos de Ciência da Computação e Matemática.
Projetos de pesquisa
Coordenador do projeto CT-INFO 506598/04-7: Simulação Algorítmica, Semântica e Aplicações da Computação
Coordenador do projeto UNIVERSAL 471791/2004-0: Teoria Semântica, Lógica e Aplicações da Computação
9/2003 - 2/2007Outras atividades técnico-científicas , Instituto de Ciências Exatas, Departamentos de Ciência da Computação e Matemática.
Atividade realizada
Bolsista de Pesquisa do CNPq (Nível 2: 2003-07; Nível 1D 2007-10).
8/2001 - 2004Atividades de Participação em Projeto, Instituto de Ciências Exatas, .
Projetos de pesquisa
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.
10/2001 - 12/2003Outras atividades técnico-científicas , Instituto de Ciências Exatas, Departamento de Matemática.
Atividade realizada
Coordenador do projeto "Teoria e Semântica da Computação", Edital Universal 01/2001, CNPq 47488/01-6.
01/1996 - 12/2002Ensino, 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)
3/2002 - 9/2002Outras atividades técnico-científicas , Instituto de Ciências Exatas, Departamento de Matemática.
Atividade realizada
Bolsista de pesquisa do programa de incentivo à pesquisa da Fundção de Estudos em Ciências Matemáticas - FEMAT: Cálculos de substituições explícitas e unificação de ordem superios - O caso dos padrões de ordem superior -.
3/1999 - 8/1999Outras atividades técnico-científicas , Instituto de Ciências Exatas, Departamento de Matemática.
Atividade realizada
Bolsista de Pesquisa do programa de incentivo à produção científica da Fundação de Estudos em Ciências Matemáticas - FEMAT: Teoria de Reescrita, Teoria de Tipos e Problemas de Unificação Aritmética.
1/1996 - 8/1999Conselhos, 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 - 1999Extensã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 - 1999Outras atividades técnico-científicas , Instituto de Ciências Exatas, Departamento de Matemática.
Atividade realizada
Membro Comitê Interno PIBIC-UnB/CNPq.
8/1996 - 7/1998Conselhos, 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 - 1998Outras atividades técnico-científicas , Instituto de Ciências Exatas, Departamento de Matemática.
Atividade realizada
Coordenador projeto de pesquisa FAP-DF 193033/96: 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..
1997 - 1998Outras atividades técnico-científicas , Instituto de Ciências Exatas, Departamento de Matemática.
Atividade realizada
Participação em projeto PROIN/CAPES para modernização do ensino do cálculo.
1997 - 1997Outras atividades técnico-científicas , Instituto de Ciências Exatas, Departamento de Matemática.
Atividade realizada
Coordenador da "Escola de Verão". Projeto institucional CNPq 453687/96-2 com recursos adicionais da CAPES, FINEP e COLCIENCIAS.
1996 - 1997Outras atividades técnico-científicas , Instituto de Ciências Exatas, Departamento de Matemática.
Atividade realizada
Coordenador do projeto institucional FAP-DF 193099/95: Atualização da Capacidade Computacional do Laboratório de Cálculo.
1995 - 1997Outras atividades técnico-científicas , Instituto de Ciências Exatas, Departamento de Matemática.
Atividade realizada
Co-coordenador do projeto FAP-DF 193363/95: Métodos Computacionais e Otimização.
Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPq, Brasil.
Vínculo institucional
2003 - Atual Vínculo: Colaborador, Enquadramento Funcional: Consultor ad-hoc, Carga horária: 0
Atividades
9/2003 - 10/2007Conselhos, Comissões e Consultoria, Ciências Exatas e da Terra, .
Cargo ou função
Consultor Ad-hoc.
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/2002Pesquisa e desenvolvimento , Fachbereich Informatik, Ag Computer Systems.
Linhas de pesquisa
Aplicações da teoria da reescrita no desenvolvimento de hardware
3/1990 - 9/1991Ensino, Fachbereich Informatik, Nível: Graduação.
Disciplinas ministradas
Algoritmos Eficientes
Especificação Algébrica
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/1988Ensino, 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/1986Ensino, 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/1988Ensino, 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)
Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco, FACEPE, Brasil.
Vínculo institucional
2002 - 2007 Vínculo: Colaborador, Enquadramento Funcional: Consultor ad-hoc, Carga horária: 0
Atividades
2/2002 - 04/2007Conselhos, Comissões e Consultoria, Ciências Exatas e da Terra, .
Cargo ou função
Consultor ad-hoc.
Fundação de Amparo à Pesquisa do Estado de São Paulo, FAPESP, Brasil.
Vínculo institucional
2001 - 2001 Vínculo: Colaborador, Enquadramento Funcional: Consultor ad-hoc, Carga horária: 0
Fundação de Apoio à Pesquisa do Distrito Federal, FAP/DF, Brasil.
Vínculo institucional
2001 - 2001 Vínculo: Colaborador, Enquadramento Funcional: Consultor ad-hoc, Carga horária: 0
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.

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

Projetos de Pesquisa
2012 - 2013Coordenador do projeto de cooperação internacional STIC-AmSud Brasil/França/Argentina (CAPES/INRIA/MINCYT, Edital 2011), Desenvolvimento Formal de Programas e Aplicações - DeCoPA
Descrição: Aplicação de cálculos de sustituições explícitas e teoria de tipos no desenvolvimento formal de programas computacionais. 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: Em andamento; Natureza: Pesquisa.
Alunos envolvidos: Mestrado acadêmico ( 1) Doutorado ( 3) .
Integrantes: Flávio Leonardo Cavalcanti de Moura - Integrante / Edward Hermann Haeusler - Integrante / Daniel Lima Ventura - Integrante / Delia Kesner - Integrante / Alejandro Ríos - Integrante / Elaine Pimentel - Integrante / Galdino, André L. - Integrante / Andréia Borges Avelar - Integrante / Daniele Nantes Sobrinho - Integrante / Ana Cristina Rocha Oliveira - Integrante / Eduardo Bonelli - Integrante / Antonio Bucciarelli - Integrante / Mauricio Ayala Rincon - Coordenador.
Financiador(es): CAPES - Centro Anhanguera de Promoção e Educação Social - Auxílio financeiro..
2010 - 2013Coordenador 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 PQ CNPq dos Programas de Pós em Matemática e Informática da UnB..
Situação: Em andamento; Natureza: Pesquisa.
Integrantes: Mauricio Ayala Rincon - Coordenador.
Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro / Fundação de Apoio à Pesquisa do Distrito Federal - Auxílio financeiro..
2010 - 2012Coordenador 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: Flávio Leonardo Cavalcanti de Moura - Integrante / Daniel Lima Ventura - Integrante / Cláudia Nalon - Integrante / Andréia Borges Avelar - Integrante / Daniele Nantes Sobrinho - Integrante / Mauricio Ayala Rincon - Coordenador.
Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.Número de orientações: 2.
2008 - 2010Coordenador 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: Flávio Leonardo Cavalcanti de Moura - Integrante / Alba Cristina Magalhaes Alves de Melo - Integrante / Cláudia Nalon - Integrante / Guilherme Albuquerque Pinto - Integrante / Mauricio Ayala Rincon - Coordenador.
Financiador(es): Fundação de Apoio à Pesquisa do Distrito Federal - Auxílio financeiro.Número de orientações: 2.
2008 - 2010Coordenador 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: Jürgen Becker - Coordenador / Mauricio Ayala Rincon - Integrante.
Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.
Número de produções C, T & A: 1.
2008 - 2009Participação em Projeto PROBRAL (CAPES/DAAD), Processo 304/08, Formally Designed Reconfigurable Architectures for High Performance Applications
Descrição: Projeto de cooperação entre as Universidadaes de Brasília, Universidade Federal de Rio Grande do Sul e a Universität Karlsruhe. Coordenador Brasileiro Ricardo P. Jacobi; Coordenador Alemão Jürgen Becker..
Situação: Em andamento; Natureza: Pesquisa.
Integrantes: Reiner W Hartenstein - Integrante / Ricardo P Jacobi - Integrante / Carlos Llanos - Integrante / Jürgen Becker - Integrante / Ricardo A L Reis - Integrante / Sergio Bampi - Integrante / Mauricio Ayala Rincon - Coordenador.
.
2005 - 2007Coordenador 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 profissionalizante ( 0) / Doutorado ( 1) .
Integrantes: 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 / Mauricio Ayala Rincon - Coordenador.
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: 4.
2005 - 2007Coordenador 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 profissionalizante ( 0) / Doutorado ( 2) .
Integrantes: 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 / Mauricio Ayala Rincon - Coordenador.
Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.
Número de produções C, T & A: 2.
2001 - 2004Coordenador 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 profissionalizante ( 0) / Doutorado ( 1) .
Integrantes: 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 / Mauricio Ayala Rincon - Coordenador.
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: 7 / Número de orientações: 3.
2001 - AtualParticipação em projeto conjunto 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 do programa Auxílio Complementar à Pesquisa DPP/UnB e EPSR
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: Em andamento; Natureza: Pesquisa.
Alunos envolvidos: Graduação ( 4) / Especialização ( 0) / Mestrado acadêmico ( 3) / Mestrado profissionalizante ( 0) / Doutorado ( 2) .
Integrantes: 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 / Mauricio Ayala Rincon - Coordenador.
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.

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

Revisor de periódico
2006 - 2007 Periódico: Journal of Algorithms
2004 - 2005 Periódico: Theoretical Computer Science
2001 - 2001 Periódico: The Computer Journal
2000 - 2001 Periódico: Journal of Symbolic Computation
2002 - Atual Periódico: Journal of Automated Reasoning
1999 - 2000 Periódico: Journal of Logic and Computation
1996 - 2005 Periódico: The Logical Journal of the Interst Group on Applied Logic
2009 - 2009 Periódico: Ars Combinatoria
2010 - 2010 Periódico: JICS. Journal of Integrated Circuits and Systems (Ed. Português)
2010 - 2010 Periódico: Journal of Signal Processing Systems
2011 - Atual Periódico: ACM Transactions on Reconfigurable Technology and Systems

Á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
2009Nomeado "Professor" da Universidad Autónoma de Bucaramanga UNAB, Reitoria da UNAB (Reitor: Alberto Montoya Puyana) e SCC (Presidente: Eduardo Carrillo Zambrano).
2009Prêmio Pesquisador do Distrito Federal, classificado em segundo lugar na Categoria Exatas e da Terra, Fundação de Apoio à Pesquisa do Distrito Federal FAPDF.
2009Orientador 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..
2007Melhores Trabalhos CLEI 2007, CLEI.
2006Synplicity 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.
2006Melhores Trabalhos SBCCI 2006, SBCCI 2006.
2004Woody 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.
2002Prê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.
2002Woody 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.
2002Orientação do Melhor Projeto da Área de Ciências Exatas. Aluno: Marcos de Andrade Gomes, PIBIC/CNPq/UnB.
1999Orientação do Melhor Projeto da Área de Ciências Exatas. Aluno: Alison H. R. da Silva, PIBIC/CNPq/UnB.
1996Paraninfo, Formandos em Ciência da Computação, Universidade de Brasília.


Produção em C,T & A
Produção bibliográfica
Citações
SCOPUS
Total de trabalhos49Total de citações63  
Ayala-Rincon, M  Data: 13/12/2011
Artigos completos publicados em periódicos
1.   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.
2. ARBOLEDA, Daniel Muñoz ; SANCHEZ, D. F. ; LLANOS, Carlos ; Ayala-Rincón, Mauricio . Tradeoff of FPGA Design of a Floating-point Library for Arithmetic Operators. JICS. Journal of Integrated Circuits and Systems (Ed. Português), v. 5, p. 42-52, 2010.
3. Ventura, D. ; Ayala-Rincon, M. ; Kamareddine, F. . Explicit substitutions calculi with one step Eta-reduction decided explicitly. Logic Journal of the IGPL, v. 17, p. 697-718, 2009.
4. MOURA, Flávio Leonardo Cavalcanti de ; M. Ayala-Rincón ; KAMAREDDINE, Fairouz . Higher-Order Unification: a structural relation between Huet's method and the one based on explicit substitutions (comunicado por Dov M. Gabbay). Journal of Applied Logic, Holanda, v. 6, p. 72-108, 2008.
5. ARBOLEDA, Daniel Muñoz ; LLANOS, Carlos ; M. Ayala-Rincón ; van ELS, R. . Distributed approach to group control of elevator systems using fuzzy logic and FPGA implementation of dispatching algorithms. Engineering Applications of Artificial Intelligence, v. 21, p. 1309-1320, 2008.
6. GALDINO, André Luiz ; AYALARINCON, M . A Formalization of Newman's and Yokouchi's Lemmas in a Higher-Order Language. Journal of Formalized Reasoning, v. 1, p. 39-50, 2008.
7. GALDINO, André Luiz ; AYALARINCON, M . A Theory for Abstract Reduction Systems in PVS. CLEI Electronic Journal, v. 11, p. 1-12, 2008.
8. BOUKERCHE, Azzedine ; MELO, Alba Cristina Magalhaes Alves de ; SANDES, Edans Flávius de Oliveira ; M. Ayala-Rincón . An Exact Parallel Algorithm to Compare Very Long Biological Sequences in Clusters of Workstations. Cluster Computing, USA, v. 10, p. 187-202, 2007.
9. M. Ayala-Rincón ; ABREU, Bruno T de ; SIQUEIRA, José de . A Variant of the Ford-Johnson Algorithm that is more Space Efficient (comunicado por F. M. auf der Heide). Information Processing Letters, Holanda, v. 102, p. 201-207, 2007.
10. BOUKERCHE, Azzedine ; MELO, Alba Cristina Magalhaes Alves de ; M. Ayala-Rincón ; WALTER, Maria Emilia Machado Telles . Parallel Strategies for Local Biological Sequence Alignment. Journal of Parallel and Distributed Computing, Holanda, v. 67, n. 2, p. 170-185, 2007.
11. M. Ayala-Rincón ; LLANOS, Carlos ; JACOBI, Ricardo P ; HARTENSTEIN, Reiner W . Prototyping Time and Space Effiicient Computations of Algebraic Operations over Dynamically Reconfigurable Systems Modeled by Rewriting-Logic. ACM Transactions on Design Automation of Electronic Systems, USA, v. 11, n. 2, p. 251-281, 2006.
12. MOURA, Flávio Leonardo Cavalcanti de ; M. Ayala-Rincón ; KAMAREDDINE, Fairouz . SUBSEXPL: a Tool for Simulating and Comparing Explicit Substitutions Calculi. Journal of Applied Non-Classical Logics, Paris, v. 16, n. 1-2, p. 119-150, 2006.
13.   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.
14. JACOBI, Ricardo P ; M. Ayala-Rincón ; CARVALHO, Luis G A ; LLANOS, Carlos ; HARTENSTEIN, Reiner W . Reconfigurable Systems for Sequence Alignment and for General Dynamic Programming. Genetics and Molecular Research, Brasil, v. 4, n. 3, p. 543-552, 2005.
15. KAMAREDDINE, Fairouz ; MONIN, François ; M. Ayala-Rincón . On Automating the Extraction of Programs from Termination Proofs. Revista Colombiana de Computación, v. 4, n. 2, p. 29-48, 2004.
16. M. Ayala-Rincón ; CONEJO, P. D. . A Linear Time Lower Bound on McCreight and General Updating Algorithms for Suffix Trees. Algorithmica, New York, v. 37, n. 3, p. 233-241, 2003.
17. M. Ayala-Rincón ; KAMAREDDINE, Fairouz . On applying the lambda s_e-style of unification for simple typed higher-order unification in the pure lambda-calculus. Matemática Contemporânea, v. 24, p. 1-22, 2003.
18. M. Ayala-Rincón ; HARTENSTEIN, Reiner W ; NETO, R. M. ; JACOBI, Ricardo P ; LLANOS, Carlos . Architectural Specification, Exploration and Simulation Through Rewriting-Logic. Revista Colombiana de Computación, Colômbia, v. 3, n. 2, p. 20-34, 2003.
19. M. Ayala-Rincón ; FONSECA, A. F. ; POUBEL, Haydée Werneck ; SIQUEIRA, José de . A Framework to Visualize Equivalences Between Computational Models of Regular Languages. Information Processing Letters, v. 84, n. 1, p. 5-16, 2002.
20. M. Ayala-Rincón ; ARAÚJO, I. E. T. . Unification Modulo Presburger Arithmetic and Other Decidable Theories. Revista Colombiana de Computación, v. 2, n. 2, p. 7-19, 2002.
21. M. Ayala-Rincón ; FONSECA, A. F. ; SILVA, A. H. R. ; POUBEL, Haydée Werneck ; SIQUEIRA, José de . Animation of Relations Between Computational Models and Languages. Bulletin of the European Association for Theoretical Computer Science, v. 74, p. 235-241, 2001.
22.   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.
23. M. Ayala-Rincón ; Cesar Munoz . Explicit Substitutions and All That. Revista Colombiana de Computación, v. 1, n. 1, p. 47-71, 2000.
24.   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.
25. M. Ayala-Rincón ; L. M. R. Gadelha . Some Applications Of (Semi-)Decision Algorithms For Presburger Arithmetic In Automated Deduction Based On Rewriting Techniques. Revista de la Sociedad Chilena de Ciencia de la Computación, Chile, v. 2, n. 1, p. 14-23, 1997.
26. M. Ayala-Rincón . Problemas Actuales en el Campo de La Reescritura. Revista de la Escuela Colombiana de Ingeniería, Bogotá, Colômbia, v. 4, n. 10, p. 27-31, 1993.
Livros publicados/organizados ou edições
1. Ayala-Rincon, M. (Org.) ; 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. 200 p.
2. AYALARINCON, M (Org.) ; 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). 110 p.
3. Ayala-Rincon, M. (Org.) ; KAMAREDDINE, Fairouz (Org.) . Proceedings of the 4th Logical and Semantic Frameworks with Applications LSFA 2009. Electronic Notes in Theoretical Computer Science vol. 256. Amsterdam: Elsevier, Electronic Notes in Theoretical Computer Science, 2009. v. 256. 140 p.
4. M. Ayala-Rincón (Org.) ; HAEUSLER, Edward Hermann (Org.) . Proceedings 2nd Workshop on Logical and Semantic Frameworks, with Applications, Electronic Notes in Theoretical Computer Science, Vol 205. Amsterdam: Elsevier ENTCS - Electronic Notes in Theoretical Computer Science, 2008. v. 205. 129 p.
5. M. Ayala-Rincón (Org.) ; 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. 70 p.
6. M. Ayala-Rincón (Org.) ; QUEIROZ, R. G. (Org.) . Pre-Proc. Eighth Workshop on Logic, Language, Information and Computation. Brasília: CESPE/UnB, 2001. v. 1. 155 p.
Capítulos de livros publicados
1. 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.
2.   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. de Moura, F.L.C. ; Barbosa, A.V. ; Ayala-Rincón, Mauricio ; Kamareddine, F. . A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi. In: Logical and Semantic Frameworks with Applications, 2011, Natal. ELSEVIER ENTCS Proceedings Fifth Logical and Semantic Frameworks with Applications (LSFA 2010). Amsterdam : Elsevier. v. 269. p. 41-54.
2. 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.
3. 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.
4. 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.
5. Avelar, Andréia B ; GALDINO, André Luiz ; de Moura, F.L.C. ; Ayala-Rincon, M. . A Formalization of the Theorem of Existence of First-Order Most General Unifiers. In: Logical and Semantic Frameworks with Applications LSFA 2011, 2011, Belo Horizonte. Pre-Proc. 6th Logical and Semantic Frameworks with Applications, 2011. p. 1-16.
6. 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. Pre-Proc. 9th International Workshop on Reduction Strategies in Rewriting and Programming WRS 2009. v. 15. p. 69-82.
7. 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.
8. 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.
9. 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.
10. 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.
11. 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.
12. 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.
13. 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.
14. 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.
15. Galdino, André L. ; Ayala-Rincón, Mauricio . A PVS Theory for Term Rewriting Systems. In: Third Workshop on Logical and Semantic Frameworks, with Applications - LSFA, 2009, Salvador. ELSEVIER ENTCS Proceedings Third Logical and Semantic Frameworks, with Applications LSFA 2008. Amsterdam : Elsevier. v. 247. p. 67-83.
16. 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.
17. 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.
18. 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.
19. 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.
20. 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.
21. 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.
22. 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.
23. 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.
24. 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.
25. 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.
26. 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.
27. 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.
28. 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.
29. 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.
30. 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.
31. 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.
32. 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.
33. 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.
34. 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.
35. 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.
36. 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.
37. 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.
38. M. Ayala-Rincón ; JACOBI, Ricardo P ; CARVALHO, Luis G A ; LLANOS, Carlos ; HARTENSTEIN, Reiner W . Modeling and Prototyping Dynamically Reconfigurable Systems for Efficient Computations of Dynamic Programming Methods by Rewriting-Logic. In: 17th Symposium on Integrated Circuits and System Design - SBCCI 04, 2004, Porto Galhinas. Proc. Symposium on Integrated Circuits and System Design, 2004. p. 248-253.
39. 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.
40. 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.
41. 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.
42. 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.
43. 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.
44. 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.
45. 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.
46. M. Ayala-Rincón ; NETO, R. M. ; JACOBI, Ricardo P ; HARTENSTEIN, Reiner W ; LLANOS, Carlos . 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 Workshop on Reduction Strategies in Rewriting and Programming - WRS02. Wien, Austria : Verlag Berger, 2002. p. 127-141.
47. 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.
48. 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.
49. 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.
50. 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.
51. 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.
52. 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.
53. 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.
54. 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.
55. 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.
56. 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.
57. 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.
58. 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.
59. 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. 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.
2. 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. 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.
2. 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.
3. 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.
4. 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.
5. 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.
6. 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.
7. 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.
8. 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.
9. 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.
10. 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.
11. 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.
12. 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.
13. 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 . 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 . 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 . 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 . Expressivenes of Conditional Equational Systems with Built-in Predicates. Bulletin of the European Association for Theoretical Computer Science, v. 53, p. 485-486, 1994.
Demais tipos de produção bibliográfica
1. M. Ayala-Rincón . Fundamentos de Programação Lógica e Funcional - O princípio de resolução e a teoria de reescrita -. Brasília: Departamento de Matemática, Universidade de Brasília, 2003 (Livro).
2. 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).
3. 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).
4. 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).
5. 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).
6. 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).
7. 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
Softwares com registro de patente
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.
Softwares sem registro de patente
1. Ayala-Rincon, M. ; Cesar Munoz ; Goodloe, Alwyn . Terminação pelo "size-change principle" via grafos de contextos de chamados em PVS. 2010.
2. Avelar, Andréia B ; GALDINO, André Luiz ; Ayala-Rincon, M. . unification, uma teoria PVS para unificação em sistemas de primeira ordem. 2009.
3. GALDINO, André Luiz ; AYALARINCON, M . TRS - PVS theory for term rewriting systems. 2008.
4. GALDINO, André Luiz ; AYALARINCON, M . ARS - PVS theory for abstract reduction systems. 2007.
5. 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.
6. 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.
7. 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.
8. 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.
9. 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.
10. M. Ayala-Rincón ; L. M. R. Gadelha . Algoritmo de decisão para a aritmética de Presburger. 1995.
Trabalhos técnicos
1. Ayala-Rincon, M. . Membro do Comitê Julgador 1a rodada Edital MCT/SETEC/CNPq Nº 075/2010 RHAE Pesquisador na Empresa. 2011.
2. Ayala-Rincón, Mauricio . Membro do Comitê de Seleção de Bolsistas Doutorado e Sandúiche DAAD/CNPq-CAPES. 2011.
3. Ayala-Rincon, M. . Membro do Comitê Julgador 2a rodada Edital MCT/SETEC/CNPq Nº 075/2010 RHAE Pesquisador na Empresa. 2011.
4. Ayala-Rincon, M. . Membro do Comitê Julgador 3a rodada Edital MCT/SETEC/CNPq Nº 075/2010 RHAE Pesquisador na Empresa. 2011.
5. Ayala-Rincon, M. . Membro do Comitê Julgador 1a rodada Edital MCT/SETEC/CNPq Nº 062/2009 RHAE Pesquisador na Empresa. 2010.
6. Ayala-Rincon, M. . Membro do Comitê Julgador 2a rodada Edital MCT/SETEC/CNPq Nº 062/2009 RHAE Pesquisador na Empresa. 2010.
7. Ayala-Rincon, M. . Membro do Comitê Julgador 3a rodada Edital MCT/SETEC/CNPq Nº 062/2009 RHAE Pesquisador na Empresa. 2010.
8. AYALARINCON, M . Membro do Comitê Julgador 1a Rodada do Edital MCT/SETEC/CNPq nº 67/2008 - RHAE Pesquisador na Empresa. 2009.
9. AYALARINCON, M . Membro do Comitê de Seleção de bolsistas DAAD/CNPq/CAPES. 2009.
10. Ayala-Rincón, Mauricio . Membro do Comitê Julgador 2a Rodada do Edital MCT/SETEC/CNPq nº 67/2008 - RHAE Pesquisador na Empresa. 2009.
11. Ayala-Rincón, Mauricio . Membro do Comitê Julgador 3a Rodada do Edital MCT/SETEC/CNPq nº 67/2008 - RHAE Pesquisador na Empresa. 2009.
12. Ayala-Rincón, Mauricio . Consultor ad hoc em Ciência da Computação Edital PRONEX MCT/CNPq/FAPERGS 008/2009. 2009.
13. AYALARINCON, M . Membro do Comitê Julgador, Edital MCT/CNPq/CT-Amazônia Nº 055/2008 - CT-Amazônia. 2008.
14. AYALARINCON, M . Membro do Comitê Julgador 1a Rodada do Edital MCT/SETEC/CNPq nº 32/2007 - RHAE Pesquisador na Empresa. 2008.
15. AYALARINCON, M . Membro do Comitê Julgador, 2a Rodada do Edital MCT/SETEC/CNPq nº 32/2007 - RHAE Pesquisador na Empresa. 2008.
16. AYALARINCON, M . Membro do Comitê Julgador PROBRAL (CAPES/DAAD) edital 2006. 2006.

Bancas
Participação em bancas examinadoras
Dissertações
1. 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.
2. 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.
3. 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.
4. 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.
5. 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.
6. 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.
7. 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.
8. 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. 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.
2. 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.
3. 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.
4. M. Ayala-Rincón; KESNER, Delia; SZASZ, Nora; RÍOS, Alejandro. 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.
5. 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. 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.
2. 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.
3. 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.
4. 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.
5. 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.
6. 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.
7. 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.
8. 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.
9. 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.
10. 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. 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.
2. 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
1. VIII Southern Programable Logic Conference SPL.Membro do Comitê Científico. 2012. (Congresso).
2. Séptimo Congreso Colombiano de Computación - 7CCC.Membro do Comitê Científico do Séptimo Congreso Colombiano de Computación - 7CCC. 2012. (Congresso).
3. PhD forum - IEEE CS Annual Symposium on VLSI.Membro do Comitê Julgador do PhD forum do 2012 ISVLSI. 2012. (Congresso).
4. Sexto Congreso Colombiano de Computación - 6CCC.Palestra convidada: Aplicação de Técnicas Formais para Verificação e Automação de Propriedades de Sisteas Computacionais. 2011. (Congresso).
5. 21st International Conference on Field Programable Logic and Applications FPL 2011.Membro do Comitê Científico. 2011. (Congresso).
6. PhD forum IEEE CS annual Symposium on VLSI.Membro do Comitê do Programa do ISVLSI 2010 PhD Forum. 2011. (Simpósio).
7. Sixth Logical and Semantic Frameworks, with Applications - LSFA 2011.Membro do Comitê do Programa LSFA 2011. 2011. (Simpósio).
8. 24rd Symposium on Integrated Circuits and Systems Design - SBCCI 2011.Membro do Comitê do Programa SBCCI 2011. 2011. (Simpósio).
9. 20th International Conference on Field Programable Logic and Applications FPL 2010.Membro do Comitê Científico. 2010. (Congresso).
10. Quinto Congreso Colombiano de Computación - 5CCC.Membro do Comitê de Programa V CCC 2010. 2010. (Congresso).
11. PhD forum IEEE CS annual Symposium on VLSI.Membro do Comitê de Programa PhD Forum ISVLSI 2010. 2010. (Congresso).
12. Fifth Logical and Semantic Frameworks, with Applications - LSFA 2010.Membro do Comitê de Programa LSFA 2010. 2010. (Congresso).
13. Reconfigurable Communication-centric Systems on Chip - ReCoSoC 2010.Palestra convidada: Automatizing the verification of the termination property of algorithms and processes. 2010. (Congresso).
14. SEMISH - XXXVII Seminário Integrado de Software e Hardware.Membro do Comitê de Programa SEMISH 2010. 2010. (Seminário).
15. 23rd Symposium on Integrated Circuits and Systems Design - SBCCI 2010.Membro do Comitê de Programa SBCCI 2010. 2010. (Simpósio).
16. Cuarto Congreso Colombiano de Computación - 4CCC.Palestra convidada: Rewriting, Types, Proofs and Veri ed Software & Hardware. 2009. (Congresso).
17. Fourth Logical and Semantic Frameworks, with Applications - LSFA 2009.Co-chair Comitê de Programa do LSFA 2009. 2009. (Congresso).
18. 9th International Workshop on Reduction Strategies in Rewriting and Programming - WRS 2009.Membro do Comitê Científico do 9th WRS 2009. 2009. (Congresso).
19. 19th International Conference on Field Programmable Logic and Applications - FPL 2009.Membro do Comitê Científico. 2009. (Congresso).
20. 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).
21. 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).
22. 22nd Symposium on Integrated Circuits and Systems Design - SBCCI 2009.Membro do Comitê de Programa SBCCI 2009. 2009. (Simpósio).
23. I Simpósio de Matemática Industrial SIMMI.Palestra convidada: Rewriting Theory, Type Theory, Proof Theory and Verification. 2009. (Simpósio).
24. 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).
25. 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).
26. 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).
27. 18th International Conference on Field Programmable Logic and Applications - FPL 2008.Membro do Comitê Científico. 2008. (Congresso).
28. Third Wokrshop on Logical and Semantic Frameworks, with Applications - LSFA 2008.Membro do Comitê Científico. 2008. (Congresso).
29. 21st Symposium on Integrated Circuits and Systems Design - SBCCI 2008.Membro do Comitê de Programa SBCCI 2008. 2008. (Congresso).
30. 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).
31. 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).
32. 20th Symposium on Integrated Circuits and Systems Design - SBCCI 2007.Membro do Comitê Científico. 2007. (Congresso).
33. Second Wokrshop on Logical and Semantic Frameworks, with Applications - LSFA 2007.Co-chair Comitê de Programa do LSFA 2007. 2007. (Congresso).
34. XXXIII Conferencia Latinoamericana de Informática - CLEI 2007.Membro do Comitê Científico. 2007. (Congresso).
35. 14th Reconfigurable Architectures Workshop RAW 2007.Membro do Comitê Científico. 2007. (Congresso).
36. 17th International Conference on Field Programmable Logic and Applications - FPL 2007.Membro do Comitê Científico. 2007. (Congresso).
37. 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).
38. Regional Meeting on Reconfigurable Computing RMRC.Membro do Comitê de Programa, Regional Meeting on Reconfigurable Computing RMRC. 2007. (Encontro).
39. 19th Symposium on Integrated Circuits and Systems Design - SBCCI 2005.Membro do Comitê de Programa SBCCI 2006. 2006. (Congresso).
40. 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).
41. Wokrshop on Logical and Semantic Frameworks, with Applications - LSFA 2006.Co-chair Comitê de Programa do LSFA 2006. 2006. (Congresso).
42. 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).
43. XXXI Conferencia Latinoamericana de Informática - CLEI 2005.Membro do Comitê de Programa CLEI 2005. 2005. (Congresso).
44. Concurso de Teses e Dissertações - CTD 2004 (Congresso da SBC 2004).Membro do Comitê de Programa CDT/SBC 2004. 2004. (Outra).
45. Workshop on Logic, Language, Information and Computation - WoLLIC 2002.Membro do Comitê de Programa WoLLIC 2002. 2002. (Congresso).
46. 5th Latin American Symposium on Theoretical Informatic LATIN 2002.Membro do Comitê de Programa LATIN 2002. 2002. (Congresso).
47. Thirty Five years of Automath.Membro do Comitê de Programa 35 years of Automath. 2002. (Congresso).
48. 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).
49. 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).
50. Festival Workshop in Foundations and Computations.Session Chair: Festival Workshop in Foundations and Computations. 2000. (Outra).
Organização de eventos
1. PIMENTEL, E. ; Della Rocca, Simona Ronchi ; Ayala-Rincon, M. ; HAEUSLER, Edward Herman . Sixth Workshop on Logical and Semantic Frameworks, with Applications - LSFA 2011 - Membro do Comitê Organizador. 2011. (Congresso).
2. Ayala-Rincon, M. ; Giesl, Juergen ; KIRCHNER, C. ; Lucas, Salvador ; Middeldorp, Aart ; OOSTROM, V. V. . Sixth International School on Rewriting. Membro do Steering Committee ISR 2012. 2011. (Outro).
3. AYALARINCON, M ; QUEIROZ, R. G. ; MOURA, Flávio Leonardo Cavalcanti de ; NALON, Cláudia . Workshop on Logic, Language, Information and Computation - WoLLIC 2010. 2010. (Congresso).
4. KIRCHNER, C. ; Middeldorp, Aart ; Ayala-Rincon, M. ; OOSTROM, V. V. . Fifth International School on Rewriting. Membro do Steering Committee ISR 2010. 2010. (Outro).
5. TREINEN, R. ; CURIEN, P. ; M. Ayala-Rincón . Federated Conference on Rewriting, Deduction, and Programming - RDP 2009. Conference Chair. 2009. (Congresso).
6. AYALARINCON, M ; MOURA, Flávio Leonardo Cavalcanti de . Fourth International School on Rewriting - ISR 2009 - Organising co-Chair. 2009. (Outro).
7. NALON, Cláudia ; PIMENTEL, E. ; PINTO, G. A. ; M. Ayala-Rincón ; HAEUSLER, Edward Hermann . Fourth Workshop on Logical and Semantic Frameworks, with Applications - LSFA 2009 - Membro do Comitê Organizador. 2009. (Congresso).
8. PIMENTEL, E. ; BENEVIDES, M. ; M. Ayala-Rincón ; HAEUSLER, Edward Hermann . Third Wokrshop on Logical and Semantic Frameworks, with Applications - LSFA 2008. 2008. (Congresso).
9. QUEIROZ, R. G. ; KAMAREDDINE, Fairouz ; M. Ayala-Rincón ; HODGES, W. . Workshop on Logic, Language, Information and Computation - WoLLIC 2008. 2008. (Congresso).
10. M. Ayala-Rincón ; HAEUSLER, Edward Hermann . Second Wokrshop on Logical and Semantic Frameworks, with Applications - LSFA 2007. 2007. (Congresso).
11. BRAGA, Christiano ; M. Ayala-Rincón ; HAEUSLER, Edward Hermann . Wokrshop on Logical and Semantic Frameworks, with Applications - LSFA 2006. 2006. (Congresso).
12. QUEIROZ, R. G. ; M. Ayala-Rincón ; HAEUSLER, Edward Hermann . Workshop on Logic, Language, Information and Computation - WoLLIC 2001. 2001. (Congresso).

Orientações
Orientações em andamento
Dissertação de mestrado
1. Daniel Saad Nogueira Nunes. Algoritmos eficientes para processamento combinatório de sequências. Início: 2011. Dissertação (Mestrado em Informática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. (Orientador).
2. José Luis Soncco. Computação Evolutiva em Bioinformática. Início: 2011. Dissertação (Mestrado em Informática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. (Orientador).
3. Fábio Henrique da Silva. Expansibilidade em cálculos de substituições explícitas. Início: 2010. Dissertação (Mestrado em Informática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. (Orientador).
4. Ana Cristina Rocha Oliveira. Formalização de propriedades de sistemas de reescrita e cálculos de substituições explícitas. Início: 2009. Dissertação (Mestrado em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico. (Orientador).
Tese de doutorado
1. Thaynara Arielly de Lima. Análise algébrico e combinatório do problema de rearranjo com técnicas de teoria de reescrita. Início: 2010. Tese (Doutorado em Matemática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. (Orientador).
2. Andréia Borges Avelar. Formalização de Critérios de Terminação e Implementação de Estratégias de Terminação de Sistemas de Reescrita. Início: 2010. Tese (Doutorado em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico. (Orientador).
3. Liliane do Nascimento Vale. Terminação via princípio de mudança de tamanho para linguagens com sintaxe elaborada. Início: 2010. Tese (Doutorado em Informática) - Universidade de Brasília. (Orientador).
4. Daniele Nantes Sobrinho. Aplicaçao da Teoria de Prova e da Teoria de Reescrita em Criptografia. Início: 2009. Tese (Doutorado em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico. (Orientador).
Iniciação científica
1. Yuri Santos Rego. Verificação formal em PVS de propriedades de segurança de sistemas criptográficos. Início: 2011. Iniciação científica (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico. (Orientador).
2. Jéssyca Cristine Lima de Souza. Formalização aplicada em problemas de otimização. Início: 2011. Iniciação científica (Graduando em Matemática) - Universidade de Brasília, Conselho Nacional de Desenvolvimento Científico e Tecnológico. (Orientador).
Orientações de outra natureza
1. Yuri Cosic Lavinas. Geração de material didático para lógica computacional. Início: 2011. Orientação de outra natureza. Universidade de Brasília. Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. (Orientador).
Supervisões e orientações concluídas
Dissertação de mestrado
1. 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.
2. 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.
3. 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.
4. 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.
5. 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.
6. 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.
7. 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.
8. 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.
9. 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.
10. 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.
11. 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.
12. 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. Co-Orientador: Mauricio Ayala Rincon.
13. 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.
14. 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.
15. 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.
16. 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.
17. 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.
18. 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. 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.
2. 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. Co-Orientador: Mauricio Ayala Rincon.
3. 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.
4. 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. Daniel Lima Ventura. 2011. Universidade de Brasília, . Mauricio Ayala Rincon.
Trabalho de conclusão de curso de graduação
1. 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. 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.
2. 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.
3. 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.
4. 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.
5. 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.
6. 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.
7. 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.
8. 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.
9. 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.
10. 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.
11. 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.
12. 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.
13. 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.
14. 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.
15. 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.
16. 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.
17. 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.
18. 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.
19. 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.
20. 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.
21. 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.
22. 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.
23. 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.
24. 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.
25. 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.
26. 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.
27. 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.
28. 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.
29. 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.
30. 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.
31. 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.
32. 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.
33. 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. 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.
2. 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.
Página gerada pelo Sistema Currículo Lattes em 23/02/2012 às 6:13:20