Flávio Leonardo Cavalcanti de Moura
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 associado 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.
Informações coletadas do Lattes em 16/09/2025
Acadêmico
Formação acadêmica
Doutorado em Teoria da Computação (Sanduíche)
2004 - 2005
Heriot-Watt University
Título: Um Estudo Comparativo em
Unificação de Ordem Superior via Cálculos de
Substituições Explícitas
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
Doutorado em Matemática
2002 - 2006
Universidade de Brasília, UnB
Título: Um Estudo Comparativo em
Unificação de Ordem Superior via Cálculos de
Substituições Explícitas
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.
Mestrado em Matemática
2000 - 2002
Universidade de Brasília, UnB
Título: Comparando Cálculos de Substituições Explícitas com Eta- conversão
, Ano de Obtenção: 2002.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 TerraGrande Á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).
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.
Idiomas
Inglês
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.
Português
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.
Francês
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.
Áreas de atuação
Grande área: Ciências Exatas e da Terra / Área: Matemática / Subárea: Matemática Aplicada/Especialidade: Teoria da Computação.
Organização de eventos
de Moura, F.L.C. . 12th Workshop on Logical and Semantic Frameworks with Applications. 2017. (Congresso).
de Moura, F.L.C. . 9th Workshop on Logical and Semantic Frameworks, with Applications. 2014. (Congresso).
de Moura, F.L.C. . 17th Workshop on Logic, Language, Information and Computation. 2010. (Congresso).
de Moura, F.L.C. . 5th Workshop on Logical and Semantic Frameworks, with Applications. 2010. (Congresso).
de Moura, F.L.C. . International School on Rewriting - ISR'09. 2009. (Outro).
de MOURA, F. L. C. . Federated Conference on Rewriting, Deduction, and Programming - RDP 2009. Conference Chair. 2008. (Organização de evento/Congresso).. 2008. (Congresso).
de Moura, F.L.C. . Second Workshop on Logical and Semantic Frameworks, with Applications. 2007. (Congresso).
Participação em eventos
SBMF08 - Simpósio Brasileiro de Métodos Formais 2008.The Correctness of the AKS Primality Test in Coq. 2008. (Simpósio).
X Curso de Qualidade - Sociedade Brasileira de Computação. 2008. (Oficina).
XXVIII CSBC - Congresso da Sociedade Brasileira de Computação. 2008. (Congresso).
10th Brazilian Symposium on Formal Methods - SBMF'07. 2007. (Simpósio).
14th Workshop on Logic, Language, Information and Computation - WoLLIC'07. 2007. (Congresso).
Second Workshop on Logical and Semantic Frameworks, with Applications - LSFA'07. 2007. (Encontro).
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).
XIV Encontro Brasileiro de Lógica.Third-Order Matching via Explicit Substitutions. 2006. (Encontro).
IWIL 2004 - 5th International Workshop on the Implementation of logics.A Framework for Simulating and Comparing Explicit Substitutions Calculi. 2005. (Encontro).
LPAR 2004 - 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning. Second-Order Matching via Explicit Substitutions. 2005. (Congresso).
ICCL Summer School. 2004. (Outra).
Second International Joint Conference on Automated Reasoning - IJCAR'04. Understanding Higher-Order Unification and Patterns. 2004. (Congresso).
10th Workshop on Logic, Language, Information and Computation. 2003. (Congresso).
7th Brazilian Symposium on Programming Languages. 2003. (Simpósio).
9th Workshop on Logic, Language, Information and Computation. Comparing Calculi of Explicit Substitutions with Eta-reduction. 2002. (Congresso).
8th Workshop onLogic, Language, Information and Computation - WoLLIC2001. 2001. (Congresso).
Participação em bancas
Flávio L. C. de Moura; NALON, C.; NANTES SOBRINHO, D.. Um provador de teoremas baseado em tableaux para verificação de propriedades temporais de conhecimento ou crença. 2015. Dissertação (Mestrado em Ciência da Computação) - Universidade de Brasília.
Flávio L. C. de Moura; M. Ayala-Rincón; ARBOLEDA, D. M. M.. Verificação de implementações em hardware e por meio de provas de correção de suas definições recursivas. 2014. Dissertação (Mestrado em Ciência da Computação) - Universidade de Brasília.
AYALA-RINCÓN, M.; E. H. Hauesler; GALDINO, A.;de MOURA, F. L. C.. 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.
AYALA-RINCÓN, M.; A. C. A. Nascimento;de MOURA, F. L. C.. Verificação Formal de Protocolos Criptográficos - O caso dos protocolos em Cascata. 2008. Dissertação (Mestrado em Informática) - Universidade de Brasília.
P. H. A. Rodrigues;de MOURA, F. L. C.; M. J. de Souza. 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.
Flávio L. C. de Moura; M. Ayala-Rincón. Formalização da Automação da Terminação através de Grafos com Matrizes de Medida. 2014. Tese (Doutorado em Matemática) - Universidade de Brasília.
Flávio L. C. de Moura; NALON, C.; M. Ayala-Rincón. Implementação de um Provador de Teoremas por Resolução para Lógicas Modais Normais. 2013. Trabalho de Conclusão de Curso (Graduação em Ciência da Computação) - Universidade de Brasília.
de MOURA, F. L. C.; F. B. 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.
M. F. R. Brandão;de MOURA, F. L. C.; M. A. de Carvalho. 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.
L. Lazarte;de MOURA, F. L. C.; S. G. Kalil. 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.
NALON, C.;de MOURA, F. L. C.; PINTO, G. A.. 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.
NALON, C.;de MOURA, F. L. C.; J. C. L. Ralha. 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.
F. A. C. Pinheiro;de MOURA, F. L. C.; PINTO, G. A.. 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.
Flávio L. C. de Moura. Matemática: Análise Numérica e Dinâmica dos Fluidos, Teoria da Computação, Probabilidade. 2017. Universidade de Brasília.
Flávio L. C. de Moura; M. Ayala-Rincón; NANTES SOBRINHO, D.. Exame de Qualificação de Doutorado do aluno Bruno de Assis Delboni. 2019. Universidade de Brasília.
Flávio L. C. de Moura; M. Ayala-Rincón. Exame de Qualificação de Doutorado do aluno Genildo de Jesus Nery. 2018. Universidade de Brasília.
Flávio L. C. de Moura; M. Ayala-Rincón. Exame de Qualificação de Doutorado do aluno John Freddy Moreno Lozada. 2017. Universidade de Brasília.
Flávio L. C. de Moura; M. Ayala-Rincón. Exame de Qualificação de Doutorado da aluna Gláucia Lenita Dierings. 2017. Universidade de Brasília.
Flávio L. C. de Moura; João J. C. Gondim; Marcelo M. de Carvalho. Exame de Qualificação de Mestrado do aluno Felipe Rodopoulos de Oliveira. 2017. Universidade de Brasília.
Flávio L. C. de Moura; M. Ayala-Rincón; Vander R. Alves; E. H. Hauesler. Exame de Qualificação de Doutorado da aluna Ariane Alves Almeida. 2016. Universidade de Brasília.
Flávio L. C. de Moura; M. Ayala-Rincón. Exame de Qualificação de Doutorado do aluno Danilo Sanção da Silveira. 2016. Universidade de Brasília.
Flávio L. C. de Moura; M. Ayala-Rincón; Vander R. Alves; E. H. Hauesler. Exame de Qualificação de Doutorado da aluna Ana Cristina Rocha Oliveira Valverde. 2014. Universidade de Brasília.
Flávio L. C. de Moura; M. Ayala-Rincón; Mario R. F. Benevides. Exame de Qualificação de Doutorado da aluna Juliana Silva Canella. 2014. Universidade de Brasília.
Flávio L. C. de Moura; M. Ayala-Rincón; Mario R. F. Benevides. Exame de Qualificação de Doutorado da aluna Lucimeire Alves de Carvalho. 2014. Universidade de Brasília.
Flávio L. C. de Moura; M. Ayala-Rincón; E. H. Hauesler. Exame de Qualificação de Doutorado do aluno Yerko Contreras Rojas. 2014. Universidade de Brasília.
Flávio L. C. de Moura; M. Ayala-Rincón; E. H. Hauesler. Exame de Qualificação de Doutorado do aluno Jhoel Estebany Sandoval Gutierrez. 2014. Universidade de Brasília.
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.
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.
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.
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.
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.
Orientou
Uma formalização do lema da substituição sem nomes locais em Coq; Início: 2024; Trabalho de Conclusão de Curso (Graduação em Engenharia de Computação) - Universidade de Brasília; (Orientador);
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;
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;
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;
Formalização em Coq da prova de confluência da cálculo lambda-x no contexto nominal; 2024; Trabalho de Conclusão de Curso; (Graduação em Engenharia de Computação) - Universidade de Brasília; Orientador: Flávio Leonardo Cavalcanti de Moura;
Formalização em Coq da prova de confluência do cálculo lambda_x; 2023; Trabalho de Conclusão de Curso; (Graduação em Engenharia de Computação) - Universidade de Brasília; Orientador: Flávio Leonardo Cavalcanti de Moura;
A formalized extension of the substitution lemma in Coq; 2023; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Universidade de Brasília; Orientador: Flávio Leonardo Cavalcanti de Moura;
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;
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;
Formalização da Normalização Forte em Cálculos com Substituições Explícitas; 2019; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade de Brasília; Orientador: Flávio Leonardo Cavalcanti de Moura;
Formalização da Confluência em Cálculos de Substituições Explícitas; 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: Flávio Leonardo Cavalcanti de Moura;
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;
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;
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;
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;
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;
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;
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;
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;
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;
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;
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;
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;
Produções bibliográficas
-
LIMA, MARIA J. D. ; de Moura, Flávio L. C. . A Formalized Extension of the Substitution Lemma in Coq. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE , v. 389, p. 80-95, 2023.
-
AVELAR, 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.
-
CARVALHO-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.
-
Avelar, Andréia B ; Galdino, André L ; de Moura, Flávio LC ; Ayala-Rincón, Mauricio . A Formalization of the Theorem of Existence of First-Order Most General Unifiers. Electronic Proceedings in Theoretical Computer Science , v. 81, p. 63-78, 2012.
-
de MOURA, F. L. C. ; Barbosa, Alex ; M. Ayala-Rincón . A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi. Electronic Notes in Theoretical Computer Science , v. 269, p. 41-54, 2011.
-
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.
-
de 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.
-
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.
-
Ayala-Rincón, Mauricio ; de Moura, Flávio L. C. . Undergraduate Topics in Computer Science. 1. ed. Springer International Publishing, 2017.
-
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 .
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
de MOURA, F. L. C. . Unification for λ-calculi Without Propagation Rules. 2016. (Apresentação de Trabalho/Congresso).
-
de MOURA, F. L. C. ; PEIXOTO, R. . The Correctness of the AKS Primality Test in Coq. 2008. (Apresentação de Trabalho/Simpósio).
Outras produções
AYALA-RINCÓN, M. ; de MOURA, F. L. C. . SUBSEXPL - uma ferramenta para comparação de cálculos de substituições explíciras. 2004.
TENENBLAT, K. ; de MOURA, F. L. C. . ACOGEO - Apoio Computacional à Geometria Diferencial. 1997.
Projetos de pesquisa
-
2022 - Atual
Projeto Universal CNPq (processo 409003/2021-2) Terminação e Estruturas Algébricas em Computação, Descrição: O objetivo principal é a exploração da aplicabilidade de diversos arcabouços formais, como a teoria de reescrita, a teoria de tipos, a teoria de prova e as estruturas algébricas, no desenvolvimento de sistemas computacionais e dedutivos e na implementação de soluções algorítmicas provadas corretas e eficientes.Sem negligenciar as aplicações, um elemento central de análise é otratamento de mecanismos dedutivos equacionais e algébricos para sistemas de raciocínio computacional via formalização de estruturas algébricas e suas propriedades, além da aplicação de técnicas das áreas de lógica, sintaxe e semântica nominal. Com esses arcabouços formais, a pesquisa realizada aproxima a teoria da prática computacional, sendo assim de grande importância e atualidade para fornecer novas técnicas para a implementação e desenho de ferramentas inovadoras de especificação (linguagens de programação e de computação simbólica, que permitem, por exemplo, implementar métodos de computação numérica) e dedução (associadas à automação do raciocínio e de processos de inferência via assistentes de provas, cerne de aplicações em Inteligência Artificial via programação lógica) que dão suporte ao desenvolvimento formal de sistemas computacionais robustos e matematicamente provados corretos.O projeto envolve cooperação com pesquisadores de AMA/NASA LaRC, King's College London, Johannes Kepler University Linz, através de implementação de visitas à UnB e co-orientações de mestrado e doutorado.. , Situação: Em andamento; Natureza: Pesquisa. , Integrantes: Flávio Leonardo Cavalcanti de Moura - Integrante / Mauricio Ayala Rincón - Coordenador / Andre Galdino - Integrante / Cláudia Nalon - Integrante / Avelar, Andréia B - Integrante / Daniele Nantes Sobrinho - Integrante / Thaynara Arielly de Lima - Integrante / Thiago Mendoça Ferreira Ramos - Integrante / Gabriel Ferreira Silva - Integrante / Ariane Alves Almeida - Integrante / Andrés Felipe González Barragán - Integrante / Ali Khãn Caires Ribeiro Santos - Integrante / Nikson Bernardes Fernandes Ferreira - Integrante.
-
2022 - Atual
Projeto Demanda Espontânea (FAPDF DE 00193.00001175/2021-11), Descrição: O projeto inclui um time de pesquisadores dos Institutos de Ciências Exatas da UnB e da UFG, assim como da UFCat e da UnB sede Planaltina. O objetivo é desenvolvimento de técnicas nominais para raciocínio equacional computacional, e a formalização no assistente de demonstração PVS de teoremas relacionados com automação da terminação de programas funcionais, assim como a formalização de teoremas algébricos para anéis não comutativos e suas aplicações.O projeto envolve cooperação com pesquisadores de AMA/NASA LaRC, King's College London, Johannes Kepler University Linz, através de implementação de visitas à UnB e co-orientações de mestrado e doutorado.. , Situação: Em andamento; Natureza: Pesquisa. , Integrantes: Flávio Leonardo Cavalcanti de Moura - Integrante / Mauricio Ayala Rincón - Coordenador / Andre Galdino - Integrante / Daniel Lima Ventura - Integrante / A B Avelar - Integrante / Daniele Nantes Sobrinho - Integrante / Thaynara Arielly de Lima - Integrante / Thiago Mendoça Ferreira Ramos - Integrante / Gabriel Ferreira Silva - Integrante / Andrés Felipe González Barragán - Integrante / Ali Khãn Caires Ribeiro Santos - Integrante / Leonardo Melo Batista - Integrante / Mehwish Arshid - Integrante.
-
2017 - 2020
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: Concluído; 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. , Integrantes: Flávio Leonardo Cavalcanti de Moura - Integrante / Andre Galdino - Integrante / Daniel Lima Ventura - Integrante / A B Avelar - Integrante / Ayala-Rincón, Mauricio - Coordenador / Daniele Nantes Sobrinho - Integrante / Ana Cristina Rocha Oliveira - Integrante / José Luis Soncco-Álvarez - Integrante / Thaynara Arielly de Lima - Integrante / Daniel Saad Nogueira Nunes - Integrante.
-
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. , Integrantes: Flávio Leonardo Cavalcanti de Moura - Integrante / Mauricio Ayala Rincón - Coordenador.
-
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. , Integrantes: Flávio Leonardo Cavalcanti de Moura - Coordenador.
-
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. , Integrantes: Flávio Leonardo Cavalcanti de Moura - Coordenador / Mauricio Ayala Rincón - Integrante / Maria Emilia M T Water - Integrante / Ricardo Pezzuol Jacobi - Integrante / Carlos Llanos - Integrante / Carlos Morra - Integrante / Michael Hubner - Integrante / Juegen Becker - Integrante / Reiner Hertenstein - Integrante.
-
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. , Integrantes: Flávio Leonardo Cavalcanti de Moura - Integrante / Mauricio Ayala Rincón - Coordenador / Hélio Carneiro Ferreira - Integrante / Andre Galdino - Integrante / Daniel Lima Ventura - Integrante / Cláudia Nalon - Integrante / Jorge C Lucero - Integrante., Número de produções C, T & A: 1
-
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. , Integrantes: Flávio Leonardo Cavalcanti de Moura - Integrante / Mauricio Ayala Rincón - Coordenador / Hélio Carneiro Ferreira - Integrante / Aline Cosme da Cunha - Integrante / Andre Galdino - Integrante / Daniel Lima Ventura - Integrante / Cláudia Nalon - Integrante., Número de produções C, T & A: 1
-
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. , Integrantes: Flávio Leonardo Cavalcanti de Moura - Integrante / Mauricio Ayala Rincón - Coordenador / Fairouz Kamareddine - Integrante / Hélio Carneiro Ferreira - Integrante / Aline Cosme da Cunha - Integrante., Número de produções C, T & A: 1
Prêmios
2004
Woody Bledsoe Student Travel Award, IJCAR 2004.
Histórico profissional
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:
Experiência profissional
2006 - Atual
Universidade de Brasília, UnBVínculo: Servidor Público, Enquadramento Funcional: Professor Adjunto, Regime: Dedicação exclusiva.
2002 - 2006
Universidade de Brasília, UnBVínculo: Estudante de doutorado, Enquadramento Funcional: Estudante de doutorado, Regime: Dedicação exclusiva.
Atividades
-
08/2006
Ensino, Ciência da Computação, Nível: Pós-GraduaçãoDisciplinas ministradas, Teoria da Computação
-
08/2006
Ensino, Bacharelado e Licenc. em Ciência da Computação, Nível: GraduaçãoDisciplinas ministradas, Introdução à Ciência da Computação, Lógica Computacional 1
-
07/2006
Pesquisa e desenvolvimento, Departamento de Ciência da Computação.Linhas de pesquisa
-
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.
Criando um monitoramento
Nossos robôs irão buscar nos nossos bancos de dados todos os processos de Flávio Leonardo Cavalcanti de Moura e sempre que o nome aparecer em publicações dos Diários Oficiais, avisaremos por e-mail e pelo painel do usuário
Criando um monitoramento
Nossos robôs irão buscar nos nossos bancos de dados todas as movimentações desse processo e sempre que o processo aparecer em publicações dos Diários Oficiais e nos Tribunais, avisaremos por e-mail e pelo painel do usuário
Confirma a exclusão?