| Applied logic for computer scientists: computational deduction and formal proofs M Ayala-Rincón, FLC De Moura Springer, 2017 | 29 | 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 | 15 | 2014 |
| 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 | 13 | 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 | 13 | 2008 |
| Second-order matching via explicit substitutions FLC de Moura, F Kamareddine, M Ayala-Rincón Logic for Programming, Artificial Intelligence, and Reasoning: 11th …, 2005 | 10 | 2005 |
| 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 | 7 | 2010 |
| 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 |
| 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 | 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 |
| 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 | 3 | 2019 |
| 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 |
| A formalization of the (compositional) z property FLC de Moura, LO Rezende Technical Report, Universidade de Brasılia, 2021 | 2 | 2021 |
| Higher-order unification via explicit substitutions at a distance FLC de Moura LSFA, 2014 | 2 | 2014 |
| 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 |
Mauricio Ayala RinconProfessor of Computer Science and Mathematics, Universidade de BrasiliaE-mail confirmado em unb.br
