Por favor, use este identificador para citar o enlazar este ítem:
https://hdl.handle.net/20.500.12008/4715
Cómo citar
Registro completo de metadatos
Campo DC | Valor | Lengua/Idioma |
---|---|---|
dc.contributor.advisor | Bove, Ana | - |
dc.contributor.advisor | Dybjer, Peter | - |
dc.contributor.author | Sicard-Ramírez, Andrés | - |
dc.date.accessioned | 2015-10-09T20:53:58Z | - |
dc.date.available | 2015-10-09T20:53:58Z | - |
dc.date.issued | 2015 | - |
dc.identifier.citation | SICARD-RAMÍREZ, A. "Reasoning about functional programs by combining interactive and automatic proofs". Tesis de Doctorado. Montevideo : Universidad de la República (Uruguay). Facultad de Ingeniería. Instituto de Computación - PEDECIBA, 2015. | es |
dc.identifier.issn | 0797-6410 | - |
dc.identifier.uri | http://hdl.handle.net/20.500.12008/4715 | - |
dc.description.abstract | We propose a new approach to computer-assisted verification of lazy functional programs where functions can be defined by general recursion. We work in first-order theories of functional programs which are obtained by translating Dybjer's programming logic (Dybjer, P. [1985]. Program Verification in a Logical Theory of Constructions. In: Functional Programming Languages and Computer Architecture. Ed. by Jouannaud, J. P. Vol. 201. Lecture Notes in Computer Science. Springer, pp. 334–349) into a first-order theory, and by extending this programming logic with new (co-)inductive predicates. Rather than building a special purpose system, we formalise our theories in Agda, a proof assistant for dependent type theory which can be used as a generic theorem prover. Agda provides support for interactive reasoning by representing first-order theories using the propositions-as-types principle. Further support is provided by off-the-shelf automatic theorem provers for first-order-logic called by a Haskell program that translates our Agda representations of first-order formulae into the TPTP language understood by the provers. We show some examples where we combine interactive and automatic reasoning, covering both proofs by induction and co-induction. The examples include functions defined by structural recursion, simple general recursion, nested recursion, higher-order recursion, guarded and unguarded co-recursion. | en |
dc.description.abstract | Proponemos un nuevo enfoque a la verificación asistida por computador de programas funcionales perezosos, en los cuales las funciones pueden ser definidas por recursión general. Empleamos teorías de primer orden para programas funcionales las cuales fueron obtenidas de traducir la lógica para la programación de Dybjer (Dybjer, P. [1985]. Program Verification in a Logical Theory of Constructions. En: Functional Programming Languages and Computer Architecture. Ed. by Jouannaud, J.-P. Vol. 201. Lecture Notes in Computer Science. Springer, págs. 334–349) a una teoría de primer orden, y de extender esta lógica para la programación con nuevos predicados (co-)inductivos. En lugar de construir un sistema para formalizar nuestras teorías, formalizamos éstas en Agda, un asistente de pruebas para teoría de tipos dependientes que puede ser usado como un demostrador de teoremas genérico. Agda proporciona soporte para el razonamiento interactivo representando las teorías de primer orden mediante el principio de propositions-as-types. Se obtiene soporte adicional mediante demostradores automáticos de teoremas genéricos para lógica de primer orden, los cuales son llamados por un programa desarrollado en Haskell, que traslada nuestra representación en Agda de las fórmulas de primer orden al lenguaje TPTP entendido por los demostradores automáticos. Mostramos ejemplos de combinación de razonamiento interactivo y automático en pruebas por inducción y por co-inducción. Nuestros ejemplos incluyen funciones definidas por recursión estructural, recursión general simple, recursión anidada, recursión de orden superior y co-recursión. | es |
dc.format.extent | 173 p. | es |
dc.format.mimetype | aplication/pdf | en |
dc.language.iso | en | es |
dc.publisher | UR.FI. | 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 | Demostración automática de teoremas | es |
dc.subject | Demostración interactiva de teoremas | es |
dc.subject | Evaluación perezosa | es |
dc.subject | Teoría de tipos | es |
dc.subject | Lenguajes totales | es |
dc.subject | Recursión general | es |
dc.subject | Teorías de primer orden | es |
dc.subject | Verificación de programas funcionales | es |
dc.subject | Automatic proofs | en |
dc.subject | First-order theories | en |
dc.subject | Functional program correctness | en |
dc.subject | General recursion | en |
dc.subject | Interactive proofs | en |
dc.subject | Lazy evaluation | en |
dc.subject | Total languages | en |
dc.subject | Type theory | en |
dc.title | Reasoning about functional programs by combining interactive and automatic proofs | es |
dc.type | Tesis de doctorado | es |
dc.contributor.filiacion | Sicard-Ramírez Andrés | - |
thesis.degree.grantor | Universidad de la República (Uruguay). Facultad de Ingeniería. | es |
thesis.degree.grantor | PEDECIBA Informática | es |
thesis.degree.name | Doctor en Informática | es |
dc.rights.licence | Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0) | es |
Aparece en las colecciones: | Tesis de posgrado - Instituto de Computación |
Ficheros en este ítem:
Fichero | Descripción | Tamaño | Formato | ||
---|---|---|---|---|---|
tesisd-sicard.pdf | 754,47 kB | Adobe PDF | Visualizar/Abrir |
Este ítem está sujeto a una licencia Creative Commons Licencia Creative Commons