Ver el código de «A Formalization of Abstract Properties of Confluent Reductions in PVS»

{| border="1"
| '''Title:''' 
| A Formalization of Abstract Properties of Confluent Reductions in PVS
|-
| '''Authors:''' 
| {{jalonso}} and {{mjoseh}}.
|-
| '''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 [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
* [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:'''
| [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].
|}