Flávio L. C. de Moura

Table of Contents

flavio2.jpg

contato@flaviomoura.mat.br

Lecturer in the Department of Computer Science and a member of the Group of Theory of Computation GTC/UnB at Universidade de Brasília.

Research interests: Rewriting Theory, Proof Theory, Type Theory and Theorem Proving.

Currículo Lattes DBLP

1 News/Notícias:

  • [2017-03-16 Qui 14:16] Oferta de bolsas de Iniciação Científica para início em abril/2017 (clique para mais informações):
    • Projetos disponíveis para trabalho em verificação formal com o assistente de provas Coq (http://coq.inria.fr)
    • Valor da bolsa: R$ 400,00 mensais
    • Requisito: IRA > 3.
    • Interessados devem enviar email para flaviomoura@unb.br ou agendar uma reunião link

2 Events/Eventos Científicos:

  1. LSFA 2017 (PC member and local organiser)
  2. SCSS 2012 (PC member)
  3. LSFA 2011 (PC member)
  4. LSFA 2010 (General Chair)
  5. WoLLIC 2010 (Organising committee)
  6. ISR 2009 (Organising committee)
  7. RDP 2009 (Organising committee)
  8. LSFA 2009 (PC member)
  9. PAAR 2008 (PC member)
  10. LSFA 2007 (PC member and local organiser)

3 Publications/Publicações:

3.2 Journals:

  • A. B. Avelar, A. L. Galdino, F. L. C. de Moura and M. Ayala-Rincón. First-order unification in the PVS proof assistant. Logic Journal of IGPL 2014.
  • F.L.C. de Moura, M. Ayala-Rincón and F. Kamareddine. Higher-Order Unification: A structural relation between Huet's method and the one based on explicit substitutions. The journal of Applied Logic, Volume 6, issue 1, pages 72-108, 2008.
  • F.L.C. de Moura, M. Ayala-Rincón and F. Kamareddine. SUBSEXPL: a Tool for Simulating and Comparing Explicit Substitutions Calculi. Journal of Applied and Non-Classical Logics, 16(1-2):119-150, Special Issue on Implementation of Logics (selected papers of IWIL-4 and IWIL-5 ), edited by Boris Konev, Renate Schmidt and Stephan Schulz, 2006.
  • M. Ayala-Rincón, F.L.C. de Moura and F. Kamareddine. Comparing and Implementing Calculi of Explicit Substitutions with Eta-Reduction. Annals of Pure and Applied Logic - WoLLIC 2002 selected papers, Ruy de Queiroz, Bruno Poizat and Sergei Artemov, Eds., Vol 134(1):5-41, 2005.

3.3 Conferences:

  • F. L. C. de Moura. Unification for λ-calculi without propagation rules. Proc. of the 13th International Colloquium on Theoretical Aspects of Computing (ICTAC 2016).
  • W. L. R. de C. Segundo, F. L. C. de Moura and D. L. Ventura. Formalizing a Named Explicit Substitutions Calculus in Coq. In CICM-WS-WiP 2014.
  • F. L. C. de Moura, D. Kesner and M. Ayala-Rincón. Metaconfluence of Calculi with Explicit Substitutions at a Distance. Proc. of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2014).
  • A.B. Avelar, F.L.C. de Moura, M. Ayala-Rincón, and A.L. Galdino. A Formalization of the Theorem of Existence of First-Order Most General Unifiers. Proc. of the 6th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2011).
  • F. L. C. de Moura and A. V. Barbosa and M. Ayala-Rincón and F. Kamareddine. A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi. Proc. 5th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2010).
  • A.B. Avelar, F.L.C. de Moura, M. Ayala-Rincón and A.L. Galdino. Verification of the Completeness of Unification Algoritms à la Robinson. Proc. of the 17th International Workshop on Logic, Language, Information and Computation (WoLLIC 2010).
  • R. B. Nogueira, A.C.A. Nascimento, F.L.C. de Moura and M. Ayala-Rincón. Formalization of Security Proofs Using PVS in the Dolev-Yao Model. Booklet Proc. Computability in Europe (CiE 2010).
  • F.L.C. de Moura, F. Kamareddine and M. Ayala-Rincón. Second-Order Matching via Explicit Substitutions. Proc. of the 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2004).
  • M. Ayala-Rincón, F.L.C. de Moura and F. Kamareddine. Comparing Calculi of Explicit Substitutions with Eta-reduction. Proc. of the 9th Workshop on Logic, Language, Information and Computation (WoLLIC 2002).

3.4 Others:

  • J. P. C. C. de Queiroz and F. L. C. de Moura. A Study about Formal Verification of Imperative Programs, 2013.
  • R. Peixoto and F.L.C. de Moura. The Correctness of the AKS Primality Test in Coq. Poster section of the XI Simpósio Brasileiro de Métodos Formais (SBMF 2008).
  • F. L. C. de Moura. Um Estudo Comparativo sobre Unificação de Ordem Superior em Cálculos de Substituições Explícitas Tese de doutorado. Universidade de Brasília, 2006.
  • F.L.C. de Moura, M. Ayala-Rincón and F. Kamareddine. SUBSEXPL: A Tool for Simulating and Comparing Explicit Substitutions Calculi. Proc. of the 5th International Workshop on the Implementation of Logics (IWIL 2004).
  • F.L.C. de Moura. Understanding Higher-Order Unification and Patterns. Contributions to the Doctoral Programme of the Second International Joint Conference on Automated Reasoning (IJCAR'04), CEUR Workshop Proceedings.
  • F. L. C. de Moura. Comparando Cálculos de Substituições Explícitas com Eta-conversão. Dissertação de mestrado. Universidade de Brasília, 2002.

4 Teaching/Ensino:

5 Physical and Postal Address/Endereço:

Departamento de Ciência da Computação
Universidade de Brasília, Edifício CIC/EST sala 03
CEP 70910-900, Asa Norte, Brasília - DF, Brazil.

Meeting request/Agendar uma reunião: Doodle

Author: Flávio L. C. de Moura

Email: contato@flaviomoura.mat.br

Created: 2017-03-25 Sáb 13:50

Validate