Publications
In Preparation
- F. L. C. de Moura, D. L. Ventura, R. S. Ramos and
F. S. Paranhos. A constructive formalisation of the Modular Strong
Normalisation Theorem.
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.
Conferences:
- 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)
- 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. Proc. of the 13th International Colloquium on Theoretical Aspects of Computing (ICTAC 2016).
- 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).
- 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.
- 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).
- 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).
- 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).
- 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).
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.