Flávio Leonardo Cavalcanti de Moura

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


Possui graduação em Bacharelado e Licenciatura em Matemática pela Universidade de Brasília (1998), mestrado em Matemática pela Universidade de Brasília (2002), doutorado em Teoria da Computação (Sanduíche) - Heriot-Watt University (2005), doutorado em Matemática pela Universidade de Brasília (2006) e pós-doutorado na Université Paris Diderot (Paris 7) (2011). Atualmente é professor adjunto da Universidade de Brasília. Tem experiência na área de Matemática, com ênfase em Teoria da Computação, atuando principalmente nos seguintes temas: cálculo lambda, substituições explícitas e unificação de ordem superior. (Texto informado pelo autor)


Identificação


Nome
Flávio Leonardo Cavalcanti de Moura
Nome em citações bibliográficas
de MOURA, F. L. C.;de Moura, F.L.C.;de Moura, Flávio LC;Flávio L. C. de Moura;de Moura, Flávio L. C.

Endereço


Endereço Profissional
Universidade de Brasília, Departamento de Ciência da Computação.
Campus Universitário Darcy Ribeiro
Asa Norte
70910900 - Brasília, DF - Brasil
Telefone: (61) 31073676
URL da Homepage: http://www.cic.unb.br/~flavio/


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


2002 - 2006
Doutorado em Matemática.
Universidade de Brasília, UnB, Brasil.
Título: Um Estudo Comparativo em Unificação de Ordem Superior via Cálculos de Substituições Explícitas, Ano de obtenção: 2006.
Orientador: Mauricio Ayala Rincón.
Bolsista do(a): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior, CAPES, Brasil.
Palavras-chave: Calculi of Explicit Substitutions; Explicit Substitutions; Higher-Order Unification; Lambda Calculus.
2004 - 2005
Doutorado em Teoria da Computação (Sanduíche).
Heriot-Watt University, HWU, Escócia.
Título: Um Estudo Comparativo em Unificação de Ordem Superior via Cálculos de Substituições Explícitas, Ano de obtenção: 2005.
Orientador: Fairouz Kamareddine.
Bolsista do(a): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior, CAPES, Brasil.
Palavras-chave: Calculi of Explicit Substitutions; Higher-Order Unification; Matching.
Grande área: Ciências Exatas e da Terra
2000 - 2002
Mestrado em Matemática.
Universidade de Brasília, UnB, Brasil.
Título: Comparando Cálculos de Substituições Explícitas com Eta- conversão,Ano de Obtenção: 2002.
Orientador: Mauricio Ayala Rincón.
Bolsista do(a): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior, CAPES, Brasil.
Palavras-chave: Substituições Explícitas; Teoria de Reescrita; Lambda Cálculo.
Grande área: Ciências Exatas e da Terra
Grande Área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação / Especialidade: Computabilidade e Modelos de Computação.
Setores de atividade: Desenvolvimento de Programas (Software).
1992 - 1998
Graduação em Licenciatura e Bacharelado em Matemática.
Universidade de Brasília, UnB, Brasil.


Pós-doutorado


2010 - 2011
Pós-Doutorado.
Université Paris Diderot, PARIS 7, França.
Grande área: Ciências Exatas e da Terra
Grande Área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação.


Atuação Profissional



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

2006 - Atual
Vínculo: Servidor Público, Enquadramento Funcional: Professor Adjunto, Regime: Dedicação exclusiva.

Vínculo institucional

2002 - 2006
Vínculo: Estudante de doutorado, Enquadramento Funcional: Estudante de doutorado, Regime: Dedicação exclusiva.

Atividades

08/2006 - Atual
Ensino, Ciência da Computação, Nível: Pós-Graduação

Disciplinas ministradas
Teoria da Computação
08/2006 - Atual
Ensino, Bacharelado e Licenc. em Ciência da Computação, Nível: Graduação

Disciplinas ministradas
Introdução à Ciência da Computação
Lógica Computacional 1
07/2006 - Atual
Pesquisa e desenvolvimento , Departamento de Ciência da Computação, .

06/2007 - 06/2007
Outras atividades técnico-científicas , Departamento de Ciência da Computação, Departamento de Ciência da Computação.

Atividade realizada
Revisão de artigos do LSFA'07 enviados por Mauricio Ayala-Rincón..
04/2007 - 04/2007
Outras atividades técnico-científicas , Departamento de Ciência da Computação, Departamento de Ciência da Computação.

Atividade realizada
Revisão de artigos de FPL07 enviados por Mauricio Ayala Rincón.
06/2005 - 06/2005
Outras atividades técnico-científicas , Departamento de Ciência da Computação, Departamento de Ciência da Computação.

Atividade realizada
Revisão de trabalhos para CLEI 2005 enviados por Mauricio Ayala-Rincón.
10/2004 - 10/2004
Outras atividades técnico-científicas , Departamento de Matemática, Departamento de Matemática.

Atividade realizada
Revisão de trabalhos para Mathematical Knowledge Management (MKM 2004) enviado por Prof. Fairouz Kamareddine. Proc. publicados em Lecture Notes in Computer Science n. 3119.


Linhas de pesquisa


1.
Lógica e semântica da computação: cálculo Lambda e cálculos de substituições explícitas


Projetos de pesquisa


2017 - Atual
Projeto Demanda Espontânea (FAPDF 193.001.369/2016) Estruturas Formais para Computação e Dedução
Descrição: Descrição: O objetivo geral da pesquisa é a exploração da aplicabilidade da teoria de reescrita, dos cálculos de substituições explícitas, da sintaxe e lógica nominal, da teoria de tipos e da teoria de prova no desenvolvimento de sistemas computacionais e na implementação de soluções algorítmicas corretas e eficientes aplicadas em diversas áreas e em particular em mecanismos de dedução equacional (casamento, unificação e estreitamento) com aplicações de destaque como raciocínio de segurança e integridade de sistemas de comunicação e protocolos criptográficos..
Situação: Em andamento; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (2) / Doutorado: (4) .
Integrantes: Flávio Leonardo Cavalcanti de Moura - Integrante / Daniel Lima Ventura - Integrante / Avelar, Andréia B - Integrante / Galdino, André L - Integrante / Mauricio Ayala Rincon - Coordenador / Daniele Nantes Sobrinho - Integrante.
2013 - 2017
Projeto UNIVERSAL 476952/2013-1 Formalização de Sistemas Computacionais com Substituições Explícitas, Terminação e Aplicações
Descrição: O objetivo geral da nossa pesquisa é a exploração da aplicabilidade da teoria de reescrita, dos cálculos de substituições explícitas, da teoria de tipos e da teoria de prova no desenvolvimento de sistemas computacionais e na implementação de soluções algorítmicas corretas e eficientes aplicadas a diversas áreas. A teoria de reescrita é um mecanismo efetivo e bem estabelecido de programação com aplicações em diversas áreas. Com efeito, diversos ambientes de programação e dedução como Maude dependem de um formalismo teórico baseado diretamente em sistemas de reescrita de ordem superior com suporte de sistemas de tipos elaborados. Ambientes de especificação bem conhecidos utilizam mecanismos essenciais da teoria de reescrita como {\em matching}, simplificação e unificação (c.f. Isabelle/HOL, Coq, $\lambda$Prolog, PVS, etc). O GTC/UnB tem desenvolvido aplicações da teoria de reescrita em contextos que vão da modelagem de {\em hardware} eficiente até a verificação de {\em software} crítico. É neste contexto que a presente proposta está focada; mais especificamente, na formalização de propriedades de cálculos de substituições explícitas e na automatização da propriedade de terminação de processos computacionais..
Situação: Concluído; Natureza: Pesquisa.
2012 - 2014
Pesquisador do projeto STIC-AmSud: Formal Development of Computer Programs and Applications (DeCoPA)
Descrição: Computer systems are becoming more and more complex. This brings along new challenges to the computer science community in terms of security, correctness, interoperability and more. We propose three convergent lines of research focused on the development of the operational semantics of modern foundational theories of programming languages. The first one explores extensions of the lambda-calculus with explicit substitutions. In particular, we are interested in a new approach, known as structural lambda-calculus that was inspired in MELL Proof-Nets and whose evaluation rules act at a distance, and the substitutions are no longer propagated over terms. The second one concerns the Pure Pattern Calculus, which is a mechanism based on pattern-matching that supports new forms of polymorphism. In fact, the pattern calculus introduces two forms of polymorphism, named path polymorphism and pattern polymorphism that treat in a uniform and simple way all kinds of data structure. Finally, the third line of research integrates the first two, and is about the formalization in proof assistants of the results obtained. Proof assistants provide a specialized environment where mathematical proofs are built to certify properties..
Situação: Concluído; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (2) / Doutorado: (3) .
Integrantes: Flávio Leonardo Cavalcanti de Moura - Integrante / Mauricio Ayala Rincón - Coordenador / Daniel Lima Ventura - Integrante / Edward Hermann Hauesler - Integrante / Delia Kesner - Integrante / Eduardo Bonelli - Integrante / Antonio Bucciarelli - Integrante.Financiador(es): CAPES - Centro Anhanguera de Promoção e Educação Social - Cooperação.
2010 - 2015
Pesquisador 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-graduação em Matemática e Informática da UnB..
Situação: Concluído; Natureza: Pesquisa.
2010 - 2012
Pesquisador do Projeto UNIVERSAL 481783/2010-5: Substituições Explícitas, Terminação e Formalização de Sistemas e Aplicações Computacionais
Situação: Concluído; Natureza: Pesquisa.
2008 - 2010
Pesquisador 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 / Mauricio Ayala Rincón - Coordenador / Cláudia Nalon - Integrante / Guilherme Albuquerque Pinto - Integrante / Alba Cristina Magalhães Alves de Melo - Integrante.Financiador(es): Fundação de Apoio à Pesquisa do Distrito Federal - Auxílio financeiro.
2008 - 2010
Pesquisador 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
Situação: Concluído; Natureza: Pesquisa.
2005 - 2007
Projeto CT-INFO: 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..
Situação: Concluído; Natureza: Pesquisa.
2005 - 2007
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.
2001 - 2011
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
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. Recursos utilizados incluem: auxílio de Projeto Universal CNPq (2002-2003), bolsa de pesquisa CNPq (2003-2007), Bolsa CAPES de Doutorado Sanduiche (2004-2005), Bolsas PIBIC/CNPq (2003-2004, 2004-2005). Recursos de participação em projeto "Métodos Determinísticos e Não Determinísticos" Programa de Apoio à Núcleos de Excelência - PRONEX, Edital 001/2003 - Convênio 0096-00/2004 SDCT/FAPDF/MCT/CNPq..
Situação: Concluído; Natureza: Pesquisa.


Áreas de atuação


1.
Grande área: Ciências Exatas e da Terra / Área: Matemática / Subárea: Matemática Aplicada/Especialidade: Teoria da Computação.


Idiomas


Português
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.
Inglês
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.
Francês
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.


Prêmios e títulos


2004
Woody Bledsoe Student Travel Award, IJCAR 2004.


Produções



Produção bibliográfica
Artigos completos publicados em periódicos

1.
AVELAR, A. B.2014AVELAR, A. B. ; GALDINO, A. L. ; de MOURA, F. L. C. ; AYALA-RINCON, M. . First-order unification in the PVS proof assistant. Logic Journal of the IGPL (Print), v. 22, p. 758-789, 2014.

2.
CARVALHO-SEGUNDO, W.2014CARVALHO-SEGUNDO, W. ; de MOURA, F. L. C. ; VENTURA, D. L. . Formalizing a Named Explicit Substitutions Calculus in Coq. CEUR Workshop Proceedings, v. 1186, p. 19, 2014.

3.
Avelar, Andréia B2012Avelar, Andréia B ; Galdino, André L ; de Moura, Flávio LC ; Ayala-Rincón, Mauricio . A Formalization of the Theorem of Existence of First-Order Most General Unifiers. Electronic Proceedings in Theoretical Computer Science, v. 81, p. 63-78, 2012.

4.
de MOURA, F. L. C.;de Moura, F.L.C.;de Moura, Flávio LC;Flávio L. C. de Moura;de Moura, Flávio L. C.2011de MOURA, F. L. C.; Barbosa, Alex ; M. Ayala-Rincón . A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi. Electronic Notes in Theoretical Computer Science, v. 269, p. 41-54, 2011.

5.
de MOURA, F. L. C.;de Moura, F.L.C.;de Moura, Flávio LC;Flávio L. C. de Moura;de Moura, Flávio L. C.2008 de MOURA, F. L. C.; AYALA-RINCÓN, M. ; KAMAREDDINE, F. . Higher-Order Unification: A structural relation between Huet's method and the one based on explicit substitutions. Journal of Applied Logic, v. 6, p. 72-108, 2008.

6.
de MOURA, F. L. C.;de Moura, F.L.C.;de Moura, Flávio LC;Flávio L. C. de Moura;de Moura, Flávio L. C.2006de MOURA, F. L. C.; AYALA-RINCÓN, M. ; KAMAREDDINE, F. . SUBSEXPL: a Tool for Simulating and Comparing Explicit Substitutions Calculi. Journal of Applied Non-Classical Logics, v. 16, p. 119-150, 2006.

7.
de MOURA, F. L. C.;de Moura, F.L.C.;de Moura, Flávio LC;Flávio L. C. de Moura;de Moura, Flávio L. C.2005 de MOURA, F. L. C.; AYALA-RINCÓN, M. ; KAMAREDDINE, F. . 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.

Livros publicados/organizados ou edições
1.
Ayala-Rincón, Mauricio ; de Moura, Flávio L. C. . Undergraduate Topics in Computer Science. 1. ed. Springer International Publishing, 2017.

2.
M. Ayala-Rincón ; de MOURA, F. L. C. . Fundamentos da Programação Lógica e Funcional - O princípio da resolução e a teoria de reescrita. 1. ed. Universidade de Brasília, 2014. 230p .

Capítulos de livros publicados
1.
de Moura, Flávio LC. Unification for λ-calculi Without Propagation Rules. In: Faro Wang, Augusto Sampaio. (Org.). Unification for λ-calculi Without Propagation Rules. 1ed.: , 2016, v. 9965, p. 179-195.

Trabalhos completos publicados em anais de congressos
1.
de MOURA, F. L. C.; D. Kesner ; M. Ayala-Rincón . Metaconfluence of Calculi with Explicit Substitutions at a Distance. In: FSTTCS 2014 - IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2014, Nova Deli. FSTTCS 2014 - IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2014.

2.
Ayala-Rincón, Mauricio ; de MOURA, F. L. C. . Computational Deduction and Formal Proofs Logic for Computation that is truly Computational. In: 8th Colombian Conference on Computation - 8CCC, 2013, Armenia. 8th Colombian Conference on Computation - 8CCC, 2013.

3.
NOGUEIRA, R. B. ; A. C. A. Nascimento ; de MOURA, F. L. C. ; AYALA-RINCÓN, M. . Formalization of Security Proofs Using PVS in the Dolev-Yao Model. In: Computability in Europe, 2010, Ponta Delgada. Computability in Europe 2010, 2010.

4.
AVELAR, A. B. ; de MOURA, F. L. C. ; GALDINO, A. ; AYALA-RINCÓN, M. . Verification of the Completeness of Unification Algorithms à la Robinson. In: 17th Workshop on Logic, Language, Information and Computation, 2010, Brasília. WoLLIC 2010, 2010.

5.
de MOURA, F. L. C.; KAMAREDDINE, F. ; AYALA-RINCÓN, M. . Second Order Matching via Explicit Substitutions. In: LPAR 2004 - 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning, 2005, Montevideo. LNAI - Lecture Notes in Artificial Intelligence, 2005. v. 3452. p. 433-448.

6.
de MOURA, F. L. C.; AYALA-RINCÓN, M. ; KAMAREDDINE, F. . SUBSEXPL: a Tool for Simulating and Comparing Explicit Substitutions Calculi. In: IWIL 2004 - 5th International Workshop on the Implementation of logics, 2005, Montevideo. Proc. 5th International Workshop on the Implementation of Logics, 2005. p. 16-30.

7.
de MOURA, F. L. C.; AYALA-RINCÓN, M. ; KAMAREDDINE, F. . Comparing Calculi of Explicit Substitutions with Eta-reduction. In: 9th Workshop on Logic, Language, Information and Computation, 2002, Rio de Janeiro. Proceedings of the 9th Workshop on Logic, Language, Information and Computation. Amsterdam: Elsevier ENTCS, 2002. v. 67. p. 77-96.

Resumos expandidos publicados em anais de congressos
1.
W L R de C Segundo ; de MOURA, F. L. C. ; VENTURA, D. L. . Formalizing a Named Explicit Substitutions Calculus in Coq. In: Conferences on Intelligent Computer Mathematics - CICM 2014, 2014, Coimbra. Workshop and Work in Progress Papers at CICM 2014, 2014. v. 1186. p. 1-10.

2.
de MOURA, F. L. C.. Higher-Order Unification via Explicit Substitutions at a Distance. In: 9th Logical and Semantic Frameworks, with Applications - LSFA 2014, 2014, Brasília. 9th Logical and Semantic Frameworks, with Applications - LSFA 2014, 2014.

3.
de MOURA, F. L. C.. Understanding Higher-Order Unification and Patterns. In: Second International Joint Conference in Automated Reasoning, 2004, Cork. CEUR Workshop Proceedings. Aachen: CEUR, 2004. v. 106.

4.
de MOURA, F. L. C.; AYALA-RINCÓN, M. ; KAMAREDDINE, F. . Animation of Reduction in the Lambda Calculus and in Calculi of Explicit Substitutions. In: XXVI Congresso Nacional de Matemática Aplicada e Computacional, 2003, São José do Rio Preto - SP. XXVI CNMAC, 2003.

Resumos publicados em anais de congressos
1.
de Moura, F.L.C.; D. Kesner ; AYALA-RINCÓN, M. . Metaconfluence of Explicit Substitutions Calculi at a Distance. In: EBL 2014 - 17th Brazilian Logic Conference, 2014, Petrópolis. EBL 2014 - 17th Brazilian Logic Conference, 2014.

2.
de MOURA, F. L. C.; AYALA-RINCÓN, M. ; KAMAREDDINE, F. . Higher-Order Unification: a structural relation between Huet's method and the one based on explicit substitution. In: XIV Encontro Brasileiro de Lógica, 2006, Itatiaia - RJ. XIV EBL, 2006.

3.
de MOURA, F. L. C.; AYALA-RINCÓN, M. ; KAMAREDDINE, F. . Third-Order Matching via Explicit Substitutions. In: XIV Encontro Brasileiro de Lógica, 2006, Itatiaia - RJ. XIV EBL, 2006.

4.
de MOURA, F. L. C.. Understanding Higher-Order Unification and Patterns. In: Second International Joint Conference on Automated Reasoning - IJCAR'04, 2004, Cork. Contributions to the Doctoral Programme of the IJCAR'04, 2004.

Apresentações de Trabalho
1.
de MOURA, F. L. C.. Unification for λ-calculi Without Propagation Rules. 2016. (Apresentação de Trabalho/Congresso).

2.
de MOURA, F. L. C.; PEIXOTO, R. . The Correctness of the AKS Primality Test in Coq. 2008. (Apresentação de Trabalho/Simpósio).


Produção técnica
Programas de computador sem registro
1.
AYALA-RINCÓN, M. ; de MOURA, F. L. C. . SUBSEXPL - uma ferramenta para comparação de cálculos de substituições explíciras. 2004.

2.
TENENBLAT, K. ; de MOURA, F. L. C. . ACOGEO - Apoio Computacional à Geometria Diferencial. 1997.



Bancas



Participação em bancas de trabalhos de conclusão
Mestrado
1.
AYALA-RINCÓN, M.; E. H. Hauesler; GALDINO, A.; de MOURA, F. L. C.. Participação em banca de Andréia Borges Avelar. Formalização da Prova de Existência de Unificadores Mais Gerais em Teorias de Primeira Ordem. 2009. Dissertação (Mestrado em Matemática) - Universidade de Brasília.

2.
AYALA-RINCÓN, M.; A. C. A. Nascimento; de MOURA, F. L. C.. Participação em banca de Rodrigo Borges Nogueira. Verificação Formal de Protocolos Criptográficos - O caso dos protocolos em Cascata. 2008. Dissertação (Mestrado em Informática) - Universidade de Brasília.

3.
P. H. A. Rodrigues; de MOURA, F. L. C.; M. J. de Souza. Participação em banca de Aline Mota de Mesquita. Uma melhora das cotas de Feng-Rao e de Miura para a distância mínima da códigos definidos sobre uma variedade afim. 2007. Dissertação (Mestrado em Matemática) - Universidade Federal de Goiás.

Trabalhos de conclusão de curso de graduação
1.
de MOURA, F. L. C.; F. B. Botelho. Participação em banca de Flávio Borges Botelho.Implementação do lambda-cálculo com tipos no software SUBSEXPL. 2008. Trabalho de Conclusão de Curso (Graduação em Bacharelado em Ciência da Computação) - Universidade de Brasília.

2.
M. F. R. Brandão; de MOURA, F. L. C.; M. A. de Carvalho. Participação em banca de Renan de Lima Barbosa e Luís Jibrim.Avaliação de infra-estrutura Tecnológica para Programas de Inclusão Digital. 2007. Trabalho de Conclusão de Curso (Graduação em Licenciatura em Ciência da Computação) - Universidade de Brasília.

3.
L. Lazarte; de MOURA, F. L. C.; S. G. Kalil. Participação em banca de Eduardo Alves Cruz de Carvalho.O moddle como ferramenta de apoio e complemento de aprendizagem: uma comparação entre a utilização e a não utilização de uma plataforma de ensino em aulas presenciais. 2007. Trabalho de Conclusão de Curso (Graduação em Licenciatura em Ciência da Computação) - Universidade de Brasília.

4.
NALON, C.; de MOURA, F. L. C.; PINTO, G. A.. Participação em banca de Cleilton Soares de Moura.Verificação de Hardware Combinacional. 2007. Trabalho de Conclusão de Curso (Graduação em Licenciatura em Ciência da Computação) - Universidade de Brasília.

5.
NALON, C.; de MOURA, F. L. C.; J. C. L. Ralha. Participação em banca de Vitor Choi.Otimização de fórmulas da lógica proposicional utilizando grafos acíclicos dirigidos. 2006. Trabalho de Conclusão de Curso (Graduação em Licenciatura em Ciência da Computação) - Universidade de Brasília.

6.
F. A. C. Pinheiro; de MOURA, F. L. C.; PINTO, G. A.. Participação em banca de Bruno Fracasso e João Belloti.Caronas UnB - Uma Ilustração do Estudo de Comunidades. 2006. Trabalho de Conclusão de Curso (Graduação em Bacharelado em Ciência da Computação) - Universidade de Brasília.



Participação em bancas de comissões julgadoras
Outras participações
1.
de MOURA, F. L. C.; AYALA-RINCÓN, M.; M E M T Walter. Exame de Qualificação de Mestrado de Washington Luís Ribeiro de C. Segundo.. 2009. Universidade de Brasília.

2.
AYALA-RINCÓN, M.; E. H. Hauesler; de MOURA, F. L. C.. Exame de qualificação de doutorado da aluna Flávia Ferreira Ramos. 2008. Universidade de Brasília.

3.
AYALA-RINCÓN, M.; E. H. Hauesler; de MOURA, F. L. C.. Exame de qualificação de doutorado do aluno Vagner Rodrigues de Bessa. 2008. Universidade de Brasília.

4.
AYALA-RINCÓN, M.; de MOURA, F. L. C.; M E M T Walter. Exame de qualificação de mestrado do aluno Leon Sólon da Silva. 2008. Universidade de Brasília.

5.
M E M T Walter; AYALA-RINCÓN, M.; de MOURA, F. L. C.; PINTO, G. A.. Exame de qualificação de mestrado da aluna Shana Schlottfeldt Santos. 2008. Universidade de Brasília.



Eventos



Participação em eventos, congressos, exposições e feiras
1.
SBMF08 - Simpósio Brasileiro de Métodos Formais 2008.The Correctness of the AKS Primality Test in Coq. 2008. (Simpósio).

2.
X Curso de Qualidade - Sociedade Brasileira de Computação. 2008. (Oficina).

3.
XXVIII CSBC - Congresso da Sociedade Brasileira de Computação. 2008. (Congresso).

4.
10th Brazilian Symposium on Formal Methods - SBMF'07. 2007. (Simpósio).

5.
14th Workshop on Logic, Language, Information and Computation - WoLLIC'07. 2007. (Congresso).

6.
Second Workshop on Logical and Semantic Frameworks, with Applications - LSFA'07. 2007. (Encontro).

7.
XIV Encontro Brasileiro de Lógica.Third-Order Matching via Explicit Substitutions. 2006. (Encontro).

8.
XIV Encontro Brasileiro de Lógica.Higher-Order Unification: a structural relation between Huet's method and the one based on explicit substitution. 2006. (Encontro).

9.
IWIL 2004 - 5th International Workshop on the Implementation of logics.A Framework for Simulating and Comparing Explicit Substitutions Calculi. 2005. (Encontro).

10.
LPAR 2004 - 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning. Second-Order Matching via Explicit Substitutions. 2005. (Congresso).

11.
ICCL Summer School. 2004. (Outra).

12.
Second International Joint Conference on Automated Reasoning - IJCAR'04. Understanding Higher-Order Unification and Patterns. 2004. (Congresso).

13.
10th Workshop on Logic, Language, Information and Computation. 2003. (Congresso).

14.
7th Brazilian Symposium on Programming Languages. 2003. (Simpósio).

15.
9th Workshop on Logic, Language, Information and Computation. Comparing Calculi of Explicit Substitutions with Eta-reduction. 2002. (Congresso).

16.
8th Workshop onLogic, Language, Information and Computation - WoLLIC2001. 2001. (Congresso).


Organização de eventos, congressos, exposições e feiras
1.
de Moura, F.L.C.. 12th Workshop on Logical and Semantic Frameworks with Applications. 2017. (Congresso).

2.
de Moura, F.L.C.. 9th Workshop on Logical and Semantic Frameworks, with Applications. 2014. (Congresso).

3.
de Moura, F.L.C.. 5th Workshop on Logical and Semantic Frameworks, with Applications. 2010. (Congresso).

4.
de Moura, F.L.C.. 17th Workshop on Logic, Language, Information and Computation. 2010. (Congresso).

5.
de Moura, F.L.C.. International School on Rewriting - ISR'09. 2009. (Outro).

6.
de MOURA, F. L. C.. Federated Conference on Rewriting, Deduction, and Programming - RDP 2009. Conference Chair. 2008. (Organização de evento/Congresso).. 2008. (Congresso).

7.
de Moura, F.L.C.. Second Workshop on Logical and Semantic Frameworks, with Applications. 2007. (Congresso).



Orientações



Orientações e supervisões em andamento
Iniciação científica
1.
Leandro Oliveira Rezende. Formalização da Confluência em Cálculos de Substituições Explícitas. Início: 2018. Iniciação científica (Graduando em Ciência da Computação) - Universidade de Brasília, Fundação de Apoio à Pesquisa do Distrito Federal. (Orientador).


Orientações e supervisões concluídas
Dissertação de mestrado
1.
João Paulo Carvalho Colu de Queiroz. Verificação Formal de Código Imperativo em Coq. 2012. Dissertação (Mestrado em Informática) - Universidade de Brasília, . Orientador: Flávio Leonardo Cavalcanti de Moura.

2.
Washington Luís Ribeiro de Carvalho Segundo. Verificação de Propriedades do Cálculo Lambda_ex em Coq. 2010. Dissertação (Mestrado em Ciência da Computação) - Universidade de Brasília, . Orientador: Flávio Leonardo Cavalcanti de Moura.

3.
Flávio Ferro Barros. Uma formalização da composicionalidade do cálculo lex em Coq. 2010. Dissertação (Mestrado em Informática) - Universidade de Brasília, . Orientador: Flávio Leonardo Cavalcanti de Moura.

Trabalho de conclusão de curso de graduação
1.
Ricardo Tadeu. Uma formalização do algoritmo AKS em Coq. 2007. Trabalho de Conclusão de Curso. (Graduação em Licenciatura em Ciência da Computação) - Universidade de Brasília. Orientador: Flávio Leonardo Cavalcanti de Moura.

2.
Flávio Botelho. Adicionando novas funcionalidades à ferramenta SUBSEXPL. 2007. Trabalho de Conclusão de Curso. (Graduação em Bacharelado em Ciência da Computação) - Universidade de Brasília. Orientador: Flávio Leonardo Cavalcanti de Moura.

Iniciação científica
1.
Nikson Bernardes Fernandes Ferreira. Formalização do Algoritmo de Ford-Johnson. 2017. Iniciação Científica. (Graduando em Ciência da Computação) - Universidade de Brasília, Fundação de Apoio à Pesquisa do Distrito Federal. Orientador: Flávio Leonardo Cavalcanti de Moura.

2.
Raphael Soares Ramos. Formalização da Modularização da Normalização Forte. 2017. Iniciação Científica. (Graduando em Ciência da Computação) - Universidade de Brasília, Fundação de Apoio à Pesquisa do Distrito Federal. Orientador: Flávio Leonardo Cavalcanti de Moura.

3.
Edson Floriano de Sousa Júnior. Formalização de Propriedades em Cálculos com Substituições Explícitas em COQ. 2015. Iniciação Científica. (Graduando em Bacharelado e Licenc. em Ciência da Computação) - Universidade de Brasília. Orientador: Flávio Leonardo Cavalcanti de Moura.

4.
Abílio Esteves Calegário de Oliveira. Correção de Sistemas Computacionais e Aplicações. 2013. Iniciação Científica. (Graduando em Ciência da Computação) - Universidade de Brasília. Orientador: Flávio Leonardo Cavalcanti de Moura.

5.
Laís Mendes Gonçalves. Portabilidade do SUBSEXPL para Emacs 23. 2013. Iniciação Científica. (Graduando em Ciência da Computação) - Universidade de Brasília. Orientador: Flávio Leonardo Cavalcanti de Moura.

6.
Luiza Alencar Azevedo. Verificação Formal de Algoritmos Criptográficos. 2012. Iniciação Científica. (Graduando em Licenciatura em Ciência da Computação) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. Orientador: Flávio Leonardo Cavalcanti de Moura.

7.
Loreane Evelyn Nazareth Brandizzi. Especificação do Cálculo Lambda es em Notação de deBruijn. 2010. Iniciação Científica. (Graduando em Licenciatura em Ciência da Computação) - Universidade de Brasília. Orientador: Flávio Leonardo Cavalcanti de Moura.

8.
Lucas de Melo Guimarães. A correção do algoritmo AKS em Coq. 2010. Iniciação Científica. (Graduando em Bacharelado em Ciência da Computação) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. Orientador: Flávio Leonardo Cavalcanti de Moura.

9.
Wilson Domingos Sidinei Alves Miranda. Formalização do Teorema de Fermat Generalizado. 2008. Iniciação Científica. (Graduando em Licenciatura e Bacharelado em Matemática) - Universidade de Brasília. Orientador: Flávio Leonardo Cavalcanti de Moura.

10.
Phillipo Lappicy Lemos Gomes. Formalização do Algoritmo AKS em Coq. 2008. Iniciação Científica. (Graduando em Licenciatura e Bacharelado em Matemática) - Universidade de Brasília, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. Orientador: Flávio Leonardo Cavalcanti de Moura.

11.
Washington Segundo. Verificação Formal de um algoritmo de matching de ordem superior em Coq. 2007. Iniciação Científica. (Graduando em Licenciatura e Bacharelado em Matemática) - Universidade de Brasília. Orientador: Flávio Leonardo Cavalcanti de Moura.

12.
Luiz Garcia. Verificação Formal de algoritmos ordenação em Coq. 2007. Iniciação Científica. (Graduando em Licenciatura em Ciência da Computação) - Universidade de Brasília. Orientador: Flávio Leonardo Cavalcanti de Moura.



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



Livros e capítulos
1.
Ayala-Rincón, Mauricio ; de Moura, Flávio L. C. . Undergraduate Topics in Computer Science. 1. ed. Springer International Publishing, 2017.

2.
M. Ayala-Rincón ; de MOURA, F. L. C. . Fundamentos da Programação Lógica e Funcional - O princípio da resolução e a teoria de reescrita. 1. ed. Universidade de Brasília, 2014. 230p .



Outras informações relevantes


Bolsista da Fundação de Estudos em Ciências Matemáticas (FEMAT) 03/2013 - 12/2013. Projeto: Modelos Funcionais de Computação e Aplicações.



Página gerada pelo Sistema Currículo Lattes em 10/12/2018 às 20:49:43