Publications

Publications (See also DBLP )

In preparation

F.L.C. de Moura, M. Ayala-Rincón and F. Kamareddine , Third-Order Matching via Explicit Substitutions.

2013

F. L. C. de Moura and M. Ayala-Rincón. Meta-confluence of Explicit Substitutions Calculi at a Distance. Submitted.
F. L. C. de Moura. Higher-Order Unification at a Distance. Submitted.
J. P. C. C. de Queiroz and F. L. C. de Moura. A Study about Formal Verification of Imperative Programs. Submitted.

2011

F.L.C. de Moura, A.V. Barbosa, M. Ayala-Rincón and F. Kamareddine. A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi, PDF. ENTCS 269:41-54 5th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2010), 2011.

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. LSFA 2011.

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, PDF. In Proc. 17th WoLLIC, LNCS vol. 6188, pag. 110-124, 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, (PDF, PVS files ). In Booklet Proc. Computability in Europe CiE, 2010.

2008

R. Peixoto and F.L.C. de Moura, The Correctness of the AKS Primality Test in Coq. XI Simpósio Brasileiro de Métodos Formais (SBMF'08) (Poster section), pdf , Coq files , 2008.

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, Elsevier, North-Holland. ISSN 1570-8683. DOI> , 2008.

2006

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, pdf , 2006.

PhD thesis (in Portuguese) pdf, 2006.

2005

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, DOI> , 2005.

F.L.C. de Moura, F. Kamareddine and M. Ayala-Rincón, Second-Order Matching via Explicit Substitutions. LPAR 2004. Springer-Verlag LNAI Volume 3452, 2005.

F.L.C. de Moura, M. Ayala-Rincón and F. Kamareddine, SUBSEXPL: A Tool for Simulating and Comparing Explicit Substitutions Calculi. 5th International Workshop on the Implementation of Logics - IWIL 2004, pdf , 2005.

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), Cork, Ireland, CEUR Workshop Proceedings, ISSN 1613-0073, online CEUR-WS.org/Vol-106 , 2004.

2002

M. Ayala-Rincón, F.L.C. de Moura and F. Kamareddine , Comparing Calculi of Explicit Substitutions with Eta-reduction ps In Pre-Proc. 9th Workshop on Logic, Language, Information and Computation - WoLLIC 2002, pages 76-96, Rio de Janeiro, Brasil, July 30 - August 2, 2002. In Vol. 67 of the Elsevier ENTCS. pdf

Master's dissertation (in Portuguese) pdf, 2002.