Comparing Calculi of Explicit Substitutions with Eta-reduction. - Mauricio Ayala-Rincón; Flávio L. C. de Moura; Fairouz Kamareddine (WoLLIC, 2002)

Understanding Higher Order Unification via Explicit Substitutions and Patterns. - Flávio L. C. de Moura (IJCAR Doctoral Programme, 2004)

Second-Order Matching via Explicit Substitutions. - Flávio L. C. de Moura; Fairouz Kamareddine; Mauricio Ayala-Rincón (LPAR, 2004)

Comparing and implementing calculi of explicit substitutions with eta-reduction. - Mauricio Ayala-Rincón; Flávio L. C. de Moura; Fairouz Kamareddine (Ann. Pure Appl. Log., 2005)

SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi. - Flávio L. C. de Moura; Mauricio Ayala-Rincón; Fairouz Kamareddine (J. Appl. Non Class. Logics, 2006)

Higher-Order Unification: A structural relation between Huet's method and the one based on explicit substitutions. - Flávio L. C. de Moura; Mauricio Ayala-Rincón; Fairouz Kamareddine (J. Appl. Log., 2008)

Verification of the Completeness of Unification Algorithms à la Robinson. - Andréia B. Avelar; Flávio L. C. de Moura; André Luiz Galdino; Mauricio Ayala-Rincón (WoLLIC, 2010)

A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi. - Flávio L. C. de Moura; A. V. Barbosa; Mauricio Ayala-Rincón; Fairouz Kamareddine (LSFA, 2010)

A Formalization of the Theorem of Existence of First-Order Most General Unifiers - Andréia B. Avelar; André Luiz Galdino; Flávio L. C. de Moura; Mauricio Ayala-Rincón (LSFA, 2011)

Metaconfluence of Calculi with Explicit Substitutions at a Distance. - Flávio L. C. de Moura; Delia Kesner; Mauricio Ayala-Rincón (FSTTCS, 2014)

Formalizing a Named Explicit Substitutions Calculus in Coq. - Washington de Carvalho Segundo; Flávio L. C. de Moura; Daniel Ventura (CICM Workshops, 2014)

First-order unification in the PVS proof assistant. - Andréia Borges Avelar; André Luiz Galdino; Flávio Leonardo Cavalcanti de Moura; Mauricio Ayala-Rincón (Log. J. IGPL, 2014)

Unification for lambda -calculi Without Propagation Rules. - Flávio L. C. de Moura (ICTAC, 2016)

Applied Logic for Computer Scientists - Computational Deduction and Formal Proofs - Mauricio Ayala-Rincón; Flávio L. C. de Moura (Springer, 2017)

The Computational Relevance of Formal Logic Through Formal Proofs. - Ariane Alves Almeida; Ana Cristina Rocha Oliveira; Thiago Mendonça Ferreira Ramos; Flávio L. C. de Moura; Mauricio Ayala-Rincón (FMTea, 2019)

A Formalized Extension of the Substitution Lemma in Coq. - Maria J. D. Lima; Flávio L. C. de Moura (FROM, 2023)