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

Investigamos 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 fu...

Full description

Autores:
Kamareddine, Fairouz
Monin, François
Ayala Rincón, Mauricio
Tipo de recurso:
Trabajo de grado de pregrado
Fecha de publicación:
2003
Institución:
Universidad Autónoma de Bucaramanga - UNAB
Repositorio:
Repositorio UNAB
Idioma:
spa
OAI Identifier:
oai:repository.unab.edu.co:20.500.12749/9046
Acceso en línea:
http://hdl.handle.net/20.500.12749/9046
Palabra clave:
Innovaciones tecnológicas
Ciencia de los computadores
Desarrollo de tecnología
Ingeniería de sistemas
Investigaciones
Tecnologías de la información y las comunicaciones
TIC´s
Technological innovations
Computer science
Technology development
Systems engineering
Investigations
Information and communication technologies
ICT's
Program extraction
Product types
Termination
ProPre system
Innovaciones tecnológicas
Ciencias de la computación
Desarrollo tecnológico
Ingeniería de sistemas
Investigaciones
Tecnologías de la información y la comunicación
Extracción de programas
Tipos de productos
Terminación
Sistema ProPre
Rights
License
Derechos de autor 2003 Revista Colombiana de Computación
id UNAB2_89c72560314ea7bb4539a40b9ee79cc2
oai_identifier_str oai:repository.unab.edu.co:20.500.12749/9046
network_acronym_str UNAB2
network_name_str Repositorio UNAB
repository_id_str
dc.title.spa.fl_str_mv Sobre la automatización de la extracción de programas de pruebas de terminación
dc.title.translated.eng.fl_str_mv On automating the extraction of programs from termination proofs
title Sobre la automatización de la extracción de programas de pruebas de terminación
spellingShingle Sobre la automatización de la extracción de programas de pruebas de terminación
Innovaciones tecnológicas
Ciencia de los computadores
Desarrollo de tecnología
Ingeniería de sistemas
Investigaciones
Tecnologías de la información y las comunicaciones
TIC´s
Technological innovations
Computer science
Technology development
Systems engineering
Investigations
Information and communication technologies
ICT's
Program extraction
Product types
Termination
ProPre system
Innovaciones tecnológicas
Ciencias de la computación
Desarrollo tecnológico
Ingeniería de sistemas
Investigaciones
Tecnologías de la información y la comunicación
Extracción de programas
Tipos de productos
Terminación
Sistema ProPre
title_short Sobre la automatización de la extracción de programas de pruebas de terminación
title_full Sobre la automatización de la extracción de programas de pruebas de terminación
title_fullStr Sobre la automatización de la extracción de programas de pruebas de terminación
title_full_unstemmed Sobre la automatización de la extracción de programas de pruebas de terminación
title_sort Sobre la automatización de la extracción de programas de pruebas de terminación
dc.creator.fl_str_mv Kamareddine, Fairouz
Monin, François
Ayala Rincón, Mauricio
dc.contributor.author.spa.fl_str_mv Kamareddine, Fairouz
Monin, François
Ayala Rincón, Mauricio
dc.contributor.googlescholar.spa.fl_str_mv Kamareddine, Fairouz [tCOuIWIAAAAJ]
Ayala Rincón, Mauricio [hd3UcpsAAAAJ]
dc.contributor.orcid.spa.fl_str_mv Ayala Rincón, Mauricio [0000-0003-0089-3905]
dc.contributor.researchgate.spa.fl_str_mv Monin, François [Francois-Monin]
Ayala Rincón, Mauricio [Mauricio-Ayala-Rincon]
dc.subject.none.fl_str_mv Innovaciones tecnológicas
Ciencia de los computadores
Desarrollo de tecnología
Ingeniería de sistemas
Investigaciones
Tecnologías de la información y las comunicaciones
TIC´s
topic Innovaciones tecnológicas
Ciencia de los computadores
Desarrollo de tecnología
Ingeniería de sistemas
Investigaciones
Tecnologías de la información y las comunicaciones
TIC´s
Technological innovations
Computer science
Technology development
Systems engineering
Investigations
Information and communication technologies
ICT's
Program extraction
Product types
Termination
ProPre system
Innovaciones tecnológicas
Ciencias de la computación
Desarrollo tecnológico
Ingeniería de sistemas
Investigaciones
Tecnologías de la información y la comunicación
Extracción de programas
Tipos de productos
Terminación
Sistema ProPre
dc.subject.keywords.eng.fl_str_mv Technological innovations
Computer science
Technology development
Systems engineering
Investigations
Information and communication technologies
ICT's
Program extraction
Product types
Termination
ProPre system
dc.subject.lemb.spa.fl_str_mv Innovaciones tecnológicas
Ciencias de la computación
Desarrollo tecnológico
Ingeniería de sistemas
Investigaciones
Tecnologías de la información y la comunicación
dc.subject.proposal.spa.fl_str_mv Extracción de programas
Tipos de productos
Terminación
Sistema ProPre
description Investigamos 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.
publishDate 2003
dc.date.issued.none.fl_str_mv 2003-12-01
dc.date.accessioned.none.fl_str_mv 2020-10-27T00:21:22Z
dc.date.available.none.fl_str_mv 2020-10-27T00:21:22Z
dc.type.coar.fl_str_mv http://purl.org/coar/resource_type/c_2df8fbb1
dc.type.driver.none.fl_str_mv info:eu-repo/semantics/article
dc.type.local.spa.fl_str_mv Artículo
dc.type.coar.none.fl_str_mv http://purl.org/coar/resource_type/c_7a1f
dc.type.redcol.none.fl_str_mv http://purl.org/redcol/resource_type/CJournalArticle
format http://purl.org/coar/resource_type/c_7a1f
dc.identifier.issn.none.fl_str_mv 2539-2115
1657-2831
dc.identifier.uri.none.fl_str_mv http://hdl.handle.net/20.500.12749/9046
dc.identifier.instname.spa.fl_str_mv instname:Universidad Autónoma de Bucaramanga UNAB
dc.identifier.repourl.none.fl_str_mv repourl:https://repository.unab.edu.co
identifier_str_mv 2539-2115
1657-2831
instname:Universidad Autónoma de Bucaramanga UNAB
repourl:https://repository.unab.edu.co
url http://hdl.handle.net/20.500.12749/9046
dc.language.iso.spa.fl_str_mv spa
language spa
dc.relation.none.fl_str_mv https://revistas.unab.edu.co/index.php/rcc/article/view/1088/1060
dc.relation.uri.none.fl_str_mv https://revistas.unab.edu.co/index.php/rcc/article/view/1088
dc.relation.references.none.fl_str_mv T. 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.
J. Giesl. Termination of nested and mutually recursive algorithms. J. of Automated Reasoning, 19:1–29, 1997.
W. 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.
F. 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.
F. 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.
F. 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.
J. L. Krivine. Lambda-calculus, Types and Models. Computers and Their Applications. Ellis Horwood, 1993.
J. L. Krivine and M. Parigot. Programming with proofs. J. Inf. Process Cybern, 26(3):149–167, 1990.
D. Leivant. Typing and computational properties of lambda expression. Theoretical Computer Science, 44:51–68, 1986.
P. 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.
P. 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.
P. Manoury and M. Simonot. Des preuves de totalit´e de fonctions comme synth`ese de programmes. PhD thesis, University Paris 7, 1992.
P. Manoury and M. Simonot. Automatizing termination proofs of recursively defined functions. Theoretical Computer Science, 135(2):319–343, 1994.
F. Monin and M. Simonot. An ordinal measure based procedure for termination of functions. Theoretical Computer Science, 254(1-2):63–94, 2001.
M. 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.
M. Parigot. Recursive programming with proofs. Theoretical Computer Science, 94(2):335–356, 1992.
dc.rights.none.fl_str_mv Derechos de autor 2003 Revista Colombiana de Computación
dc.rights.coar.fl_str_mv http://purl.org/coar/access_right/c_abf2
dc.rights.uri.*.fl_str_mv http://creativecommons.org/licenses/by-nc-sa/4.0/
dc.rights.uri.none.fl_str_mv http://creativecommons.org/licenses/by-nc-nd/2.5/co/
dc.rights.creativecommons.*.fl_str_mv Atribución-NoComercial-SinDerivadas 2.5 Colombia
rights_invalid_str_mv Derechos de autor 2003 Revista Colombiana de Computación
http://creativecommons.org/licenses/by-nc-sa/4.0/
http://creativecommons.org/licenses/by-nc-nd/2.5/co/
Atribución-NoComercial-SinDerivadas 2.5 Colombia
http://purl.org/coar/access_right/c_abf2
dc.format.mimetype.spa.fl_str_mv application/pdf
dc.publisher.none.fl_str_mv Universidad Autónoma de Bucaramanga UNAB
publisher.none.fl_str_mv Universidad Autónoma de Bucaramanga UNAB
dc.source.none.fl_str_mv Revista Colombiana de Computación; Vol. 4 Núm. 2 (2003): Revista Colombiana de Computación; 1-20
institution Universidad Autónoma de Bucaramanga - UNAB
bitstream.url.fl_str_mv https://repository.unab.edu.co/bitstream/20.500.12749/9046/1/2003_Articulo_Sobre%20la%20automatizaci%c3%b3n%20de%20la%20extracci%c3%b3n%20de%20programas%20de%20pruebas%20de%20terminaci%c3%b3n.pdf
https://repository.unab.edu.co/bitstream/20.500.12749/9046/2/2003_Articulo_Sobre%20la%20automatizaci%c3%b3n%20de%20la%20extracci%c3%b3n%20de%20programas%20de%20pruebas%20de%20terminaci%c3%b3n.pdf.jpg
bitstream.checksum.fl_str_mv 74ef5404006ce7e008df2feea5e982b9
294fee3f6361f055f09dcd583099e6ce
bitstream.checksumAlgorithm.fl_str_mv MD5
MD5
repository.name.fl_str_mv Repositorio Institucional | Universidad Autónoma de Bucaramanga - UNAB
repository.mail.fl_str_mv repositorio@unab.edu.co
_version_ 1814277788835774464
spelling Kamareddine, Fairouz1fc26ce6-d136-42a4-91ab-7430f2c065e5Monin, François3f9edcc9-bdbe-4e02-abe9-b2724eafbd88Ayala Rincón, Mauriciof681e303-3263-42cb-a9d5-96197d20d516Kamareddine, Fairouz [tCOuIWIAAAAJ]Ayala Rincón, Mauricio [hd3UcpsAAAAJ]Ayala Rincón, Mauricio [0000-0003-0089-3905]Monin, François [Francois-Monin]Ayala Rincón, Mauricio [Mauricio-Ayala-Rincon]2020-10-27T00:21:22Z2020-10-27T00:21:22Z2003-12-012539-21151657-2831http://hdl.handle.net/20.500.12749/9046instname:Universidad Autónoma de Bucaramanga UNABrepourl:https://repository.unab.edu.coInvestigamos 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.We 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.application/pdfspaUniversidad Autónoma de Bucaramanga UNABhttps://revistas.unab.edu.co/index.php/rcc/article/view/1088/1060https://revistas.unab.edu.co/index.php/rcc/article/view/1088T. 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.J. Giesl. Termination of nested and mutually recursive algorithms. J. of Automated Reasoning, 19:1–29, 1997.W. 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.F. 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.F. 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.F. 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.J. L. Krivine. Lambda-calculus, Types and Models. Computers and Their Applications. Ellis Horwood, 1993.J. L. Krivine and M. Parigot. Programming with proofs. J. Inf. Process Cybern, 26(3):149–167, 1990.D. Leivant. Typing and computational properties of lambda expression. Theoretical Computer Science, 44:51–68, 1986.P. 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.P. 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.P. Manoury and M. Simonot. Des preuves de totalit´e de fonctions comme synth`ese de programmes. PhD thesis, University Paris 7, 1992.P. Manoury and M. Simonot. Automatizing termination proofs of recursively defined functions. Theoretical Computer Science, 135(2):319–343, 1994.F. Monin and M. Simonot. An ordinal measure based procedure for termination of functions. Theoretical Computer Science, 254(1-2):63–94, 2001.M. 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.M. Parigot. Recursive programming with proofs. Theoretical Computer Science, 94(2):335–356, 1992.Derechos de autor 2003 Revista Colombiana de Computaciónhttp://creativecommons.org/licenses/by-nc-sa/4.0/http://creativecommons.org/licenses/by-nc-nd/2.5/co/Atribución-NoComercial-SinDerivadas 2.5 Colombiahttp://purl.org/coar/access_right/c_abf2Revista Colombiana de Computación; Vol. 4 Núm. 2 (2003): Revista Colombiana de Computación; 1-20Innovaciones tecnológicasCiencia de los computadoresDesarrollo de tecnologíaIngeniería de sistemasInvestigacionesTecnologías de la información y las comunicacionesTIC´sTechnological innovationsComputer scienceTechnology developmentSystems engineeringInvestigationsInformation and communication technologiesICT'sProgram extractionProduct typesTerminationProPre systemInnovaciones tecnológicasCiencias de la computaciónDesarrollo tecnológicoIngeniería de sistemasInvestigacionesTecnologías de la información y la comunicaciónExtracción de programasTipos de productosTerminaciónSistema ProPreSobre la automatización de la extracción de programas de pruebas de terminaciónOn automating the extraction of programs from termination proofsinfo:eu-repo/semantics/articleArtículohttp://purl.org/coar/resource_type/c_7a1fhttp://purl.org/coar/resource_type/c_2df8fbb1http://purl.org/redcol/resource_type/CJournalArticleORIGINAL2003_Articulo_Sobre la automatización de la extracción de programas de pruebas de terminación.pdf2003_Articulo_Sobre la automatización de la extracción de programas de pruebas de terminación.pdfArtículoapplication/pdf310029https://repository.unab.edu.co/bitstream/20.500.12749/9046/1/2003_Articulo_Sobre%20la%20automatizaci%c3%b3n%20de%20la%20extracci%c3%b3n%20de%20programas%20de%20pruebas%20de%20terminaci%c3%b3n.pdf74ef5404006ce7e008df2feea5e982b9MD51open accessTHUMBNAIL2003_Articulo_Sobre la automatización de la extracción de programas de pruebas de terminación.pdf.jpg2003_Articulo_Sobre la automatización de la extracción de programas de pruebas de terminación.pdf.jpgIM Thumbnailimage/jpeg7025https://repository.unab.edu.co/bitstream/20.500.12749/9046/2/2003_Articulo_Sobre%20la%20automatizaci%c3%b3n%20de%20la%20extracci%c3%b3n%20de%20programas%20de%20pruebas%20de%20terminaci%c3%b3n.pdf.jpg294fee3f6361f055f09dcd583099e6ceMD52open access20.500.12749/9046oai:repository.unab.edu.co:20.500.12749/90462022-11-23 14:18:08.077open accessRepositorio Institucional | Universidad Autónoma de Bucaramanga - UNABrepositorio@unab.edu.co

Publicaciones similares