Diferencia entre revisiones de «A Formalization of Abstract Properties of Confluent Reductions in PVS»
(No se muestran 14 ediciones intermedias de 2 usuarios) | |||
Línea 3: | Línea 3: | ||
| A Formalization of Abstract Properties of Confluent Reductions in PVS | | A Formalization of Abstract Properties of Confluent Reductions in PVS | ||
|- | |- | ||
− | | ''' | + | | '''Authors:''' |
− | | {{jalonso}} | + | | {{jalonso}} and {{mjoseh}}. |
|- | |- | ||
− | | ''' | + | | '''Date:''' |
| December 2009. | | December 2009. | ||
|- | |- | ||
| '''Description:''' | | '''Description:''' | ||
− | | This theory is a simple and smart formalization of abstract confluence properties such Newman's Lemma or the Church-Rosser property. This formalization is based on the paper [http://portal.acm.org/ft_gateway.cfm?id=322230&type=pdf Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems] of G. Huet. | + | | This theory is a simple and smart formalization of abstract confluence properties such as Newman's Lemma or the Church-Rosser property. This formalization is based on the paper [http://portal.acm.org/ft_gateway.cfm?id=322230&type=pdf Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems] of G. Huet. |
|- | |- | ||
− | | ''' | + | | '''Code:''' |
− | | You can find the PVS theories | + | | You can find the PVS theories |
+ | * [http://www.cs.us.es/~mjoseh/pub/TeoriasPVS/Version_PVS-3.2/FM.tgz Version PVS-3.2]. | ||
+ | * [http://www.cs.us.es/~mjoseh/pub/TeoriasPVS/Version_PVS-4.2/FM.tgz Version PVS-4.2]. | ||
+ | * [http://www.cs.us.es/~mjoseh/pub/TeoriasPVS/Version_PVS-5.0/FM.tgz Version PVS-5.0]. | ||
|- | |- | ||
| '''Documentation:''' | | '''Documentation:''' | ||
− | | ... | + | | [http://www.cs.us.es/~mjoseh/pub/2010-A_Formalization_of_Abstract_Properties_of_Confluent_Reductions_in_PVS.pdf A Formalization of Abstract Properties of Confluent Reductions in PVS]. |
|} | |} |
Revisión actual del 13:14 4 oct 2011
Title: | A Formalization of Abstract Properties of Confluent Reductions in PVS |
Authors: | José A. Alonso and María J. Hidalgo. |
Date: | December 2009. |
Description: | This theory is a simple and smart formalization of abstract confluence properties such as Newman's Lemma or the Church-Rosser property. This formalization is based on the paper Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems of G. Huet. |
Code: | You can find the PVS theories |
Documentation: | A Formalization of Abstract Properties of Confluent Reductions in PVS. |