Publications

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.

Books:

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.

Conferences:

  1. Flávio L. C. de Moura and Leandro O. Rezende. A Formalization of the (Compositional) Z Property.
    • pdf (short paper). Fifth Workshop on Formal Mathematics for Mathematicians (FMM 2021)
    • BibTeX
    • pdf (report)
  2. 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).
  3. F. L. C. de Moura. Unification for λ-calculi without propagation rules. Proc. of the 13th International Colloquium on Theoretical Aspects of Computing (ICTAC 2016).
  4. 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).
  5. 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.
  6. 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).
  7. 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).
  8. 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).
  9. 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).
  10. 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).
  11. 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).

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. Poster section of the XI Simpósio Brasileiro de Métodos Formais (SBMF 2008).
  3. 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.
  4. 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).
  5. 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.
  6. 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.