Publications

Table of Contents

1. In Preparation

  1. F. L. C. de Moura, D. L. Ventura, R. S. Ramos and F. S. Paranhos. A constructive formalisation of the Modular Strong Normalisation Theorem.

2. Books:

  1. Lógica Computacional e Algoritmos
  2. Applied Logic for Computer Scientists (BibTeX)
  3. Fundamentos da Programação Lógica e Funcional (BibTeX)

3. Journals:

  1. 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.
  2. 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.
  3. 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.
  4. 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.

4. Conferences:

  1. M. J. D. de Lima, F. L. C. de Moura. A formalized extension of the substitution lemma in Coq.
  2. Flávio L. C. de Moura and Leandro O. Rezende. A Formalization of the (Compositional) Z Property.
    • pdf (short paper). 5thth Workshop on Formal Mathematics for Mathematicians (FMM 2021)
    • BibTeX
    • pdf (report)
  3. Ariane A. Almeida, Ana Cristina Rocha-Oliveira, Thiago Mendonça Ferreira Ramos, Flávio L. C. De Moura and Mauricio Ayala-Rincon. The Computational Relevance of Formal Logic through Formal Proofs.
    • Formal Methods Teaching Workshop and Tutorial (FMTea 2019).
  4. F. L. C. de Moura. Unification for λ-calculi without propagation rules.
  5. F. L. C. de Moura, D. Kesner and M. Ayala-Rincón. Metaconfluence of Calculi with Explicit Substitutions at a Distance.
  6. W. L. R. de C. Segundo, F. L. C. de Moura and D. L. Ventura. Formalizing a Named Explicit Substitutions Calculus in Coq.
  7. 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.
    • pdf. 6th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2011)
    • BibTeX
  8. 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.
    • pdf. 17th International Workshop on Logic, Language, Information and Computation (WoLLIC 2010)
    • BibTeX
  9. 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.
    • pdf. 5th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2010)
    • BibTeX
  10. 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.
  11. F.L.C. de Moura, F. Kamareddine and M. Ayala-Rincón. Second-Order Matching via Explicit Substitutions.
    • pdf. 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2004).
    • DOI
    • BibTeX
  12. M. Ayala-Rincón, F.L.C. de Moura and F. Kamareddine. Comparing Calculi of Explicit Substitutions with Eta-reduction.

5. Others:

  1. J. P. C. C. de Queiroz and F. L. C. de Moura. A Study about Formal Verification of Imperative Programs, 2013.
  2. R. Peixoto and F.L.C. de Moura. The Correctness of the AKS Primality Test in Coq.
  3. F. L. C. de Moura. Um Estudo Comparativo sobre Unificação de Ordem Superior em Cálculos de Substituições Explícitas
    • pdf. Tese de doutorado. Universidade de Brasília, 2006.
    • BibTeX
  4. F.L.C. de Moura, M. Ayala-Rincón and F. Kamareddine. SUBSEXPL: A Tool for Simulating and Comparing Explicit Substitutions Calculi.
  5. F.L.C. de Moura. Understanding Higher-Order Unification and Patterns.
    • pdf. Doctoral Programme of the Second International Joint Conference on Automated Reasoning (IJCAR'04)
    • ceur-ws
    • BibTeX
  6. F. L. C. de Moura. Comparando Cálculos de Substituições Explícitas com Eta-conversão.
    • pdf. Dissertação de mestrado. Universidade de Brasília, 2002.
    • BibTeX

Author: Flávio L. C. de Moura

Email: flaviomoura@unb.br

Created: 2024-04-18 qui 15:38