Por favor, use este identificador para citar o enlazar este ítem:
https://hdl.handle.net/20.500.12008/3487
Cómo citar
Registro completo de metadatos
| Campo DC | Valor | Lengua/Idioma |
|---|---|---|
| dc.contributor.author | Severi, Paula | es |
| dc.contributor.author | Szasz, Nora | es |
| dc.date.accessioned | 2014-12-02T16:06:51Z | - |
| dc.date.available | 2014-12-02T16:06:51Z | - |
| dc.date.issued | 2002 | es |
| dc.date.submitted | 20141202 | es |
| dc.identifier.citation | SEVERI, P., SZASZ, N. "Internal program extraction in the calculus of inductive constructions". Reportes Técnicos 02-15. UR. FI – INCO, 2002. | es |
| dc.identifier.issn | 0797-6410 | es |
| dc.identifier.uri | http://hdl.handle.net/20.500.12008/3487 | - |
| dc.description.abstract | Based on the Calculus of Constructions extended with inductive definitions we present a Theory of Specifications with rules for simultaneously constructing programs and their correctness proofs. The theory contains types for representing specifications, whose corresponding notion of implementation is that of a pair formed by a program and a correctness proof. The rules of the theory are sych that in implementations the program parts appear mixed together with the proof parts. A reduction relation performs the task of separating programs from proofs. Consequently, every implementation computes to a pair composed of a program and a proof of its correctness, and so the program extraction procedure is immediate. | es |
| dc.format.extent | 14 p. | es |
| dc.format.mimetype | application/pdf | es |
| dc.language | in | es |
| dc.publisher | UR. FI – INCO. | es |
| dc.relation.ispartof | Reportes Técnicos 02-15 | es |
| dc.rights | Las obras depositadas en el Repositorio se rigen por la Ordenanza de los Derechos de la Propiedad Intelectual de la Universidad De La República. (Res. Nº 91 de C.D.C. de 8/III/1994 – D.O. 7/IV/1994) y por la Ordenanza del Repositorio Abierto de la Universidad de la República (Res. Nº 16 de C.D.C. de 07/10/2014) | es |
| dc.subject | CALCULUS OF CONSTRUCTIONS | es |
| dc.title | Internal program extraction in the calculus of inductive constructions | es |
| dc.type | Reporte técnico | es |
| dc.rights.licence | Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0) | es |
| Aparece en las colecciones: | Reportes Técnicos - Instituto de Computación | |
Ficheros en este ítem:
| Fichero | Descripción | Tamaño | Formato | ||
|---|---|---|---|---|---|
| TR0215.pdf | 221,45 kB | Adobe PDF | Visualizar/Abrir |
Este ítem está sujeto a una licencia Creative Commons Licencia Creative Commons
