5 citations · 22 across the 12 of their papers we have counts for
15 papers
Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms
Thaynara Arielly de Lima, Andréia Borges Avelar, André Luiz Galdino +1
This paper discusses the extension of the Prototype Verification System (PVS) sub-theory for rings, part of the PVS algebra theory, with theorems related to the division algorithm…
Equational Anti-Unification over Absorption Theories
Mauricio Ayala-Rincon, David M. Cerna, Andres Felipe Gonzalez Barragan +1
Interest in anti-unification, the dual problem of unification, is on the rise due to applications within the field of software analysis and related areas. For example, anti-unifica…
Proceedings 16th Logical and Semantic Frameworks with Applications
Mauricio Ayala-Rincon, Eduardo Bonelli
This volume contains the post-proceedings of the Sixteenth Logical and Semantic Frameworks with Applications (LSFA 2021). The meeting was held online on July 23-24, 2021, organised…
Teaching Interactive Proofs to Mathematicians
Mauricio Ayala-Rincón, Thaynara Arielly de Lima
This work discusses an approach to teach to mathematicians the importance and effectiveness of the application of Interactive Theorem Proving tools in their specific fields of inte…
Formalizing the Dependency Pair Criterion for Innermost Termination
Ariane Alves Almeida, Mauricio Ayala-Rincon
Rewriting is a framework for reasoning about functional programming. The dependency pair criterion is a well-known mechanism to analyze termination of term rewriting systems. Funct…
On Nominal Syntax and Permutation Fixed Points
Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho
We propose a new axiomatisation of the alpha-equivalence relation for nominal terms, based on a primitive notion of fixed-point constraint. We show that the standard freshness rela…