Formalising Confluence in PVS by Mauricio Ayala-Rincón

Get full text

Explicit substitions and all that by Mauricio Ayala Rincón, César Muñoz

Get full text

A Formalization of Newman's and Yokouchi's Lemmas in a Higher-Order Language by Andre Luiz Galdino, Mauricio Ayala-Rincón

Get full text

A Theory for Abstract Reduction Systems in PVS by Andre Luiz Galdino, Mauricio Ayala Rincon

Get full text

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

Get full text

On automating the extraction of programs from termination proofs by Fairouz Kamareddine, François Monin, Mauricio Ayala Rincón

Get full text

Unification modulo presburger arithmetic and other decidable theories by Mauricio Ayala Rincón, Ivan E. Tavares Araújo

Get full text

Formalizing the Confluence of Orthogonal Rewriting Systems by Ana Cristina Rocha Oliveira, Mauricio Ayala-Rincón

Get full text

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

Get full text

On Nominal Syntax and Permutation Fixed Points by Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho

Get full text

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

Get full text

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

Get full text