Sobre la automatización de la extracción de programas de pruebas de terminación

Vista sencilla de ítem
dc.contributor.authorKamareddine, Fairouzspa
dc.contributor.authorMonin, Françoisspa
dc.contributor.authorAyala Rincón, Mauriciospa
dc.contributor.googlescholarKamareddine, Fairouz [tCOuIWIAAAAJ]spa
dc.contributor.googlescholarAyala Rincón, Mauricio [hd3UcpsAAAAJ]spa
dc.contributor.orcidAyala Rincón, Mauricio [0000-0003-0089-3905]spa
dc.contributor.researchgateMonin, François [Francois-Monin]spa
dc.contributor.researchgateAyala Rincón, Mauricio [Mauricio-Ayala-Rincon]spa
dc.date.accessioned2020-10-27T00:21:22Z
dc.date.available2020-10-27T00:21:22Z
dc.date.issued2003-12-01
dc.description.abstractInvestigamos un sistema de síntesis de programas automatizado que se basa en el paradigma de la programación por pruebas. Para extraer automáticamente un término que calcule una función recursiva dada por un conjunto de ecuaciones, el sistema debe encontrar una prueba formal de la totalidad de la función dada. Debido al marco lógico particular, por lo general estos enfoques dificultan el uso de técnicas de terminación como las de la teoría de reescritura. Superamos esta dificultad para el sistema automatizado que consideramos explotando tipos de productos. Como consecuencia, esto permitiría la incorporación de técnicas de terminación utilizadas en otras áreas sin dejar de extraer programas.spa
dc.description.abstractenglishWe investigate an automated program synthesis system that is based on the paradigm of programming by proofs. To automatically extract a term that computes a recursive function given by a set of equations the system must nd a formal proof of the totality of the given function. Because of the particular logical framework, usually such approaches make it dicult to use termination techniques such as those in rewriting theory. We overcome this diculty for the automated system that we consider by exploiting product types. As a consequence, this would enable the incorporation of termination techniques used in other areas while still extracting programs.eng
dc.format.mimetypeapplication/pdfspa
dc.identifier.instnameinstname:Universidad Autónoma de Bucaramanga UNABspa
dc.identifier.issn2539-2115
dc.identifier.issn1657-2831
dc.identifier.repourlrepourl:https://repository.unab.edu.co
dc.identifier.urihttp://hdl.handle.net/20.500.12749/9046
dc.language.isospaspa
dc.publisherUniversidad Autónoma de Bucaramanga UNAB
dc.relationhttps://revistas.unab.edu.co/index.php/rcc/article/view/1088/1060
dc.relation.referencesT. Arts and J. Giesl. Automatically proving termination where simplification orderings fail. In Proceedings of Theory and Practice of Software Development TAPSOFT’97, volume 1214 of LNCS, pages 261–272, 1997.
dc.relation.referencesJ. Giesl. Termination of nested and mutually recursive algorithms. J. of Automated Reasoning, 19:1–29, 1997.
dc.relation.referencesW. A. Howard. The formulæ-as types notion of construction. In J. Hindley and J. Seldin, editors, To H.B. Curry: Essays on combinatory logic, lambda-calculus and formalism, pages 479–490. Academic Press, 1980.
dc.relation.referencesF. Kamareddine and F. Monin. On automating inductive and non-inductive termination methods. In Proceedings of the 5th Asian Computing Science Conference, volume 1742 of LNCS, pages 177–189, 1999.
dc.relation.referencesF. Kamareddine and F. Monin. On formalised proofs of termination of recursive functions. In Proceedings of the Int. Conf. on Principles and Practice of Declarative Programming, volume 1702 of LNCS, pages 29–46, 1999.
dc.relation.referencesF. Kamareddine, F. Monin and M. Ayala-Rinc´on. On automating the extraction of programs from proofs using product types. In Proceedings of the 9th Workshop on Logic, Language, Information and Computation, WoLLIC’2002, Volume 67 of ENTCS, 20 pages, 2002.
dc.relation.referencesJ. L. Krivine. Lambda-calculus, Types and Models. Computers and Their Applications. Ellis Horwood, 1993.
dc.relation.referencesJ. L. Krivine and M. Parigot. Programming with proofs. J. Inf. Process Cybern, 26(3):149–167, 1990.
dc.relation.referencesD. Leivant. Typing and computational properties of lambda expression. Theoretical Computer Science, 44:51–68, 1986.
dc.relation.referencesP. Manoury. A user’s friendly syntax to define recursive functions as typed lambdaterms. In Proceedings of Type for Proofs and Programs TYPES’94, volume 996 of LNCS, pages 83–100, 1994.
dc.relation.referencesP. Manoury, M. Parigot, and M. Simonot. ProPre, a programming language with proofs. In Proceedings of Logic Programming and Automated Reasoning, volume 624 of LNCS, pages 484–486, 1992.
dc.relation.referencesP. Manoury and M. Simonot. Des preuves de totalit´e de fonctions comme synth`ese de programmes. PhD thesis, University Paris 7, 1992.
dc.relation.referencesP. Manoury and M. Simonot. Automatizing termination proofs of recursively defined functions. Theoretical Computer Science, 135(2):319–343, 1994.
dc.relation.referencesF. Monin and M. Simonot. An ordinal measure based procedure for termination of functions. Theoretical Computer Science, 254(1-2):63–94, 2001.
dc.relation.referencesM. Parigot. Recursive programming with proofs: a second type theory. In Proceedings of the European Symposium on Programming ESOP’88, volume 300 of LNCS, pages 145–159, 1988.
dc.relation.referencesM. Parigot. Recursive programming with proofs. Theoretical Computer Science, 94(2):335–356, 1992.
dc.relation.urihttps://revistas.unab.edu.co/index.php/rcc/article/view/1088
dc.rightsDerechos de autor 2003 Revista Colombiana de Computación
dc.rights.accessrightsinfo:eu-repo/semantics/openAccessspa
dc.rights.creativecommonsAtribución-NoComercial-SinDerivadas 2.5 Colombia*
dc.rights.urihttp://creativecommons.org/licenses/by-nc-sa/4.0/*
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/2.5/co/
dc.sourceRevista Colombiana de Computación; Vol. 4 Núm. 2 (2003): Revista Colombiana de Computación; 1-20
dc.subjectInnovaciones tecnológicas
dc.subjectCiencia de los computadores
dc.subjectDesarrollo de tecnología
dc.subjectIngeniería de sistemas
dc.subjectInvestigaciones
dc.subjectTecnologías de la información y las comunicaciones
dc.subjectTIC´s
dc.subject.keywordsTechnological innovationseng
dc.subject.keywordsComputer scienceeng
dc.subject.keywordsTechnology developmenteng
dc.subject.keywordsSystems engineeringeng
dc.subject.keywordsInvestigationseng
dc.subject.keywordsInformation and communication technologieseng
dc.subject.keywordsICT'seng
dc.subject.keywordsProgram extractioneng
dc.subject.keywordsProduct typeseng
dc.subject.keywordsTerminationeng
dc.subject.keywordsProPre systemeng
dc.subject.lembInnovaciones tecnológicasspa
dc.subject.lembCiencias de la computaciónspa
dc.subject.lembDesarrollo tecnológicospa
dc.subject.lembIngeniería de sistemasspa
dc.subject.lembInvestigacionesspa
dc.subject.lembTecnologías de la información y la comunicaciónspa
dc.subject.proposalExtracción de programasspa
dc.subject.proposalTipos de productosspa
dc.subject.proposalTerminaciónspa
dc.subject.proposalSistema ProPrespa
dc.titleSobre la automatización de la extracción de programas de pruebas de terminaciónspa
dc.title.translatedOn automating the extraction of programs from termination proofseng
dc.type.coarhttp://purl.org/coar/resource_type/c_7a1f
dc.type.driverinfo:eu-repo/semantics/article
dc.type.hasversioninfo:eu-repo/semantics/acceptedVersion
dc.type.localArtículospa
dc.type.redcolhttp://purl.org/redcol/resource_type/CJournalArticle

Archivos

Bloque original

Mostrando 1 - 1 de 1
Miniatura
Nombre:
2003_Articulo_Sobre la automatización de la extracción de programas de pruebas de terminación.pdf
Tamaño:
302.76 KB
Formato:
Adobe Portable Document Format
Descripción:
Artículo
Descargar

Colecciones

Revista Colombiana de Computación