1. In Preparation
2. Books:
3. 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.
4. Conferences:
- M. J. D. de Lima, F. L. C. de Moura. A formalized extension of the substitution lemma in Coq.
- Flávio L. C. de Moura and Leandro O. Rezende. A Formalization of the (Compositional) Z Property.
- 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).
- F. L. C. de Moura. Unification for λ-calculi without propagation rules.
- pdf. 13th International Colloquium on Theoretical Aspects of Computing (ICTAC 2016)
- doi
- BibTeX
- F. L. C. de Moura, D. Kesner and M. Ayala-Rincón. Metaconfluence of Calculi with Explicit Substitutions at a Distance.
- pdf. Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2014)
- Erratum
- BibTeX
- W. L. R. de C. Segundo, F. L. C. de Moura and D. L. Ventura. Formalizing a Named Explicit Substitutions Calculus in Coq.
- 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.
- 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
- 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.
- 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.
- F.L.C. de Moura, F. Kamareddine and M. Ayala-Rincón. Second-Order Matching via Explicit Substitutions.
- M. Ayala-Rincón, F.L.C. de Moura and F. Kamareddine. Comparing Calculi of Explicit Substitutions with Eta-reduction.
- pdf. 9th Workshop on Logic, Language, Information and Computation (WoLLIC 2002)
- DOI
- BibTeX
5. 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.
- F. L. C. de Moura. Um Estudo Comparativo sobre Unificação de Ordem Superior em Cálculos de Substituições Explícitas
- F.L.C. de Moura, M. Ayala-Rincón and F. Kamareddine. SUBSEXPL: A Tool for Simulating and Comparing Explicit Substitutions Calculi.
- F.L.C. de Moura. Understanding Higher-Order Unification and Patterns.
- F. L. C. de Moura. Comparando Cálculos de Substituições Explícitas com Eta-conversão.