Diferencia entre revisiones de «A Formalization of Abstract Properties of Confluent Reductions in PVS»

De WikiGLC
Saltar a: navegación, buscar
 
(No se muestran 16 ediciones intermedias de 2 usuarios)
Línea 1: Línea 1:
−
* '''Title:''' A Formalization of Abstract Properties of Confluent Reductions in PVS
 
−
* '''Autores:''' {{jalonso}} y {{mjoseh}}.
 
−
* '''Fecha de realización:''' Diciembre de 2009.
 
−
* '''Abstract:''' 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 "Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems " of G. Huet.
 
−
* '''Code:''' La formalización en PVS se encuentra en ...
 
−
* '''Documentation:'''
 
−
 
 
{| border="1"
 
{| border="1"
 
| '''Title:'''  
 
| '''Title:'''  
 
| A Formalization of Abstract Properties of Confluent Reductions in PVS
 
| A Formalization of Abstract Properties of Confluent Reductions in PVS
 
|-
 
|-
−
| '''Autores:'''  
+
| '''Authors:'''  
−
| {{jalonso}} y {{mjoseh}}.
+
| {{jalonso}} and {{mjoseh}}.
 
|-
 
|-
−
| '''Fecha de realización:'''
+
| '''Date:'''
−
| Diciembre de 2009.
+
| December 2009.
 
|-
 
|-
−
| '''Abstract:'''  
+
| '''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:'''  
 
| '''Code:'''  
−
| La formalización en PVS se encuentra en ...
+
| 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.
Obtenido de «https://www.glc.us.es/web/index.php?title=A_Formalization_of_Abstract_Properties_of_Confluent_Reductions_in_PVS&oldid=1032»