Formalising Confluence in PVS

by Mauricio Ayala-Rincón
Published 2016-03-01

Explicit substitions and all that

by Mauricio Ayala Rincón, César Muñoz
Published 2000-12-01

Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model

by Mauricio Ayala-Rincón, Yuri Santos Rego
Published 2013-01-01

A Formalization of Newman's and Yokouchi's Lemmas in a Higher-Order Language

by Andre Luiz Galdino, Mauricio Ayala-Rincón
Published 2008-12-01

A Theory for Abstract Reduction Systems in PVS

by Andre Luiz Galdino, Mauricio Ayala Rincon
Published 2008-12-01

On automating the extraction of programs from termination proofs

by Fairouz Kamareddine, François Monin, Mauricio Ayala Rincón
Published 2003-12-01

Unification modulo presburger arithmetic and other decidable theories

by Mauricio Ayala Rincón, Ivan E. Tavares Araújo
Published 2001-12-01

Principal Typings in a Restricted Intersection Type System for Beta Normal Forms with De Bruijn Indices

by Daniel Ventura, Mauricio Ayala-Rincón, Fairouz Kamareddine
Published 2010-01-01

Formalizing the Confluence of Orthogonal Rewriting Systems

by Ana Cristina Rocha Oliveira, Mauricio Ayala-Rincón
Published 2013-03-01

Elementary Deduction Problem for Locally Stable Theories with Normal Forms

by Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho
Published 2013-03-01

A Formalization of the Theorem of Existence of First-Order Most General Unifiers

by Andréia B Avelar, André L Galdino, Flávio LC de Moura, Mauricio Ayala-Rincón
Published 2012-03-01

Architectural specification, exploration and simulation through rewriting-logic

by Mauricio Ayala Rincón, Reiner W. Hartenstein, Rinaldi Maya Neto, Ricardo P. Jacobi, Carlos Humberto Llanos
Published 2002-12-01