Applied Logic for Computer Scientists M Ayala-Rincón, FLC De Moura Springer International Publishing, 2017 | 31 | 2017 |
Comparing and implementing calculi of explicit substitutions with eta-reduction M Ayala-Rincón, FLC De Moura, F Kamareddine Annals of Pure and Applied Logic 134 (1), 5-41, 2005 | 21 | 2005 |
Fundamentos da Programaçao Lógica e Funcional—O princıpio de resoluçao e a teoria de reescrita— M Ayala-Rincón, FLC de Moura Editora UnB, 2014 | 16 | 2014 |
Higher-Order Unification: A structural relation between Huet's method and the one based on explicit substitutions FLC de Moura, M Ayala-Rincón, F Kamareddine Journal of Applied Logic 6 (1), 72-108, 2008 | 14 | 2008 |
First-order unification in the PVS proof assistant AB Avelar, AL Galdino, FLC de Moura, M Ayala-Rincón Logic Journal of the IGPL 22 (5), 758-789, 2014 | 12 | 2014 |
Second-order matching via explicit substitutions FLC de Moura, F Kamareddine, M Ayala-Rincón International Conference on Logic for Programming Artificial Intelligence …, 2005 | 10 | 2005 |
Formalization of security proofs using PVS in the Dolev-Yao model RB Nogueira, FLC de Moura, A Nascimento, M Ayala-Rincón Computability in Europe CiE 2010 (1.1), 1.2, 2010 | 7 | 2010 |
The computational relevance of formal logic through formal proofs AA Almeida, AC Rocha-Oliveira, TMF Ramos, FLC de Moura, ... Formal Methods Teaching: Third International Workshop and Tutorial, FMTea …, 2019 | 6 | 2019 |
Metaconfluence of calculi with explicit substitutions at a distance FLC de Moura, D Kesner, M Ayala-Rincón 34th International Conference on Foundation of Software Technology and …, 2014 | 6 | 2014 |
Verification of the Completeness of Unification Algorithms à la Robinson AB Avelar, FLC de Moura, AL Galdino, M Ayala-Rincón Logic, Language, Information and Computation: 17th International Workshop …, 2010 | 6 | 2010 |
SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi★ FLC de Moura, M Ayala-Rincón, F Kamareddine Journal of Applied Non-Classical Logics 16 (1-2), 119-150, 2006 | 4 | 2006 |
A formalization of the theorem of existence of first-order most general unifiers AB Avelar, AL Galdino, FLC de Moura, M Ayala-Rincón arXiv preprint arXiv:1203.6160, 2012 | 3 | 2012 |
The correctness of the AKS primality test in Coq FLC de Moura, R Tadeu July, 2008 | 3 | 2008 |
Comparing Calculi of Explicit Substitutions with Eta-reduction M Ayala-Rincón, FLC De Moura, F Kamareddine Electronic Notes in Theoretical Computer Science 67, 76-95, 2002 | 3 | 2002 |
Higher-order unification via explicit substitutions at a distance FLC de Moura LSFA, 2014 | 2 | 2014 |
A formalization of the (compositional) Z property FLC de Moura, LO Rezende Conference on Intelligent Computer Mathematics, 2021 | 1 | 2021 |
Metaconfluence of explicit substitutions calculi at a distance FLC de Moura, D Kesner, M Ayala-Rincón preparation, 2014 | 1 | 2014 |
Third-Order Matching via Explicit Substitutions FLC de Moura, M Ayala-Rincón, F Kamareddine Departamento de Matemática, Universidade de Brasılia, unpublished document …, 2005 | 1 | 2005 |
Comparando Cálculos de Substituiçoes Explıcitas com Eta-conversao FLC de Moura Brasılia, 2002 | 1 | 2002 |
A Formalized Extension of the Substitution Lemma in Coq MJD Lima, FLC de Moura arXiv preprint arXiv:2309.13801, 2023 | | 2023 |