Flávio L. C. de Moura

According to our database, Flávio L. C. de Moura authored at least 16 papers between 2002 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of five.

2023

A Formalized Extension of the Substitution Lemma in Coq.

Maria J. D. Lima, Flávio L. C. de Moura

Proceedings of the Proceedings 7th Symposium on Working Formal Methods, 2023

2019

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

Proceedings of the Formal Methods Teaching - Third International Workshop and Tutorial, 2019

2017

Applied Logic for Computer Scientists - Computational Deduction and Formal Proofs

Mauricio Ayala-Rincón, Flávio L. C. de Moura

Undergraduate Topics in Computer Science, Springer, ISBN: 978-3-319-51653-0, 2017

2016

Unification for \lambda -calculi Without Propagation Rules.

Flávio L. C. de Moura

Proceedings of the Theoretical Aspects of Computing - ICTAC 2016, 2016

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

Formalizing a Named Explicit Substitutions Calculus in Coq.

Washington de Carvalho Segundo, Flávio L. C. de Moura, Daniel Ventura

Proceedings of the Joint Proceedings of the MathUI, 2014

Metaconfluence of Calculi with Explicit Substitutions at a Distance.

Flávio L. C. de Moura, Delia Kesner, Mauricio Ayala-Rincón

Proceedings of the 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, 2014

2011

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

Proceedings of the Proceedings 6th Workshop on Logical and Semantic Frameworks with Applications, 2011

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

Proceedings of the Fifth Logical and Semantic Frameworks, with Applications Workshop, 2010

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

Proceedings of the Logic, 2010

2008

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

2006

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

2005

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

2004

Second-Order Matching via Explicit Substitutions.

Flávio L. C. de Moura, Fairouz Kamareddine, Mauricio Ayala-Rincón

Proceedings of the Logic for Programming, 2004

Understanding Higher Order Unification via Explicit Substitutions and Patterns.

Flávio L. C. de Moura

Proceedings of the Contributions to the Doctoral Programme of the 2nd International Joint Conference on Automated Reasoning, 2004

2002

Comparing Calculi of Explicit Substitutions with Eta-reduction.

Mauricio Ayala-Rincón, Flávio L. C. de Moura, Fairouz Kamareddine

Proceedings of the 9th Workhop on Logic, Language, Information and Computation, 2002