Delwedd Flaen

Internal program extraction in the calculus of inductive constructions

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 i...

Disgrifiad llawn

Wedi'i Gadw mewn:
Prif Awdur: Severi, Paula (author)
Awduron Eraill: Szasz, Nora (author)
Fformat: report
Cyhoeddwyd: 2002
Pynciau:
CALCULUS OF CONSTRUCTIONS
Mynediad Ar-lein:http://hdl.handle.net/20.500.12008/3487
Tagiau: Ychwanegu Tag
Dim Tagiau, Byddwch y cyntaf i dagio'r cofnod hwn!
_version_ 1868890146762391552
author Severi, Paula
author2 Szasz, Nora
author2_role author
author_browse Severi, Paula
Szasz, Nora
author_facet Severi, Paula
Szasz, Nora
author_role author
collection COLIBRI
dc.creator.none.fl_str_mv Severi, Paula
Szasz, Nora
dc.date.none.fl_str_mv 2002
2014-12-02T16:06:51Z
2014-12-02T16:06:51Z
20141202
dc.format.none.fl_str_mv 14 p.
application/pdf
dc.identifier.none.fl_str_mv SEVERI, P., SZASZ, N. "Internal program extraction in the calculus of inductive constructions". Reportes Técnicos 02-15. UR. FI – INCO, 2002.
0797-6410
http://hdl.handle.net/20.500.12008/3487
dc.language.none.fl_str_mv in
dc.publisher.none.fl_str_mv UR. FI – INCO.
dc.relation.none.fl_str_mv Reportes Técnicos 02-15
dc.rights.none.fl_str_mv info:eu-repo/semantics/openAccess
Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0)
dc.source.none.fl_str_mv reponame:COLIBRI
instname:Universidad de la República
instacron:Universidad de la República
dc.subject.none.fl_str_mv CALCULUS OF CONSTRUCTIONS
dc.title.none.fl_str_mv Internal program extraction in the calculus of inductive constructions
dc.type.none.fl_str_mv Reporte técnico
info:eu-repo/semantics/report
info:eu-repo/semantics/publishedVersion
description 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.
eu_rights_str_mv openAccess
format report
id anni_9dccb82e4da9a62a3bfb48ca3a390dee
identifier_str_mv SEVERI, P., SZASZ, N. "Internal program extraction in the calculus of inductive constructions". Reportes Técnicos 02-15. UR. FI – INCO, 2002.
0797-6410
instacron_str Universidad de la República
institution Universidad de la República
instname_str Universidad de la República
language_invalid_str_mv in
network_acronym_str anni
network_name_str oai-lr-anni
oai_identifier_str oai:colibri.udelar.edu.uy:20.500.12008/3487
publishDate 2002
publishDateSort 2002
publisher.none.fl_str_mv UR. FI – INCO.
reponame_str COLIBRI
repository.mail.fl_str_mv
repository.name.fl_str_mv
repository_id_str
rights_invalid_str_mv Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0)
spelling Internal program extraction in the calculus of inductive constructionsSeveri, PaulaSzasz, NoraCALCULUS OF CONSTRUCTIONSBased 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.UR. FI – INCO.2014-12-02T16:06:51Z2014-12-02T16:06:51Z200220141202Reporte técnicoinfo:eu-repo/semantics/reportinfo:eu-repo/semantics/publishedVersion14 p.application/pdfSEVERI, P., SZASZ, N. "Internal program extraction in the calculus of inductive constructions". Reportes Técnicos 02-15. UR. FI – INCO, 2002.0797-6410http://hdl.handle.net/20.500.12008/3487reponame:COLIBRIinstname:Universidad de la Repúblicainstacron:Universidad de la RepúblicainReportes Técnicos 02-15Las 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)info:eu-repo/semantics/openAccessLicencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0)oai:colibri.udelar.edu.uy:20.500.12008/34872026-04-14T10:16:13Z
spellingShingle Internal program extraction in the calculus of inductive constructions
Severi, Paula
CALCULUS OF CONSTRUCTIONS
status_str publishedVersion
title Internal program extraction in the calculus of inductive constructions
title_full Internal program extraction in the calculus of inductive constructions
title_fullStr Internal program extraction in the calculus of inductive constructions
title_full_unstemmed Internal program extraction in the calculus of inductive constructions
title_short Internal program extraction in the calculus of inductive constructions
title_sort Internal program extraction in the calculus of inductive constructions
topic CALCULUS OF CONSTRUCTIONS
url http://hdl.handle.net/20.500.12008/3487

Eitemau Tebyg