Fecha: Viernes 25 de julio de 2014
Hora: 10:30
Lugar: Sala de Posgrados, Instituto de Computación, Facultad de Ingeniería
Título de la tesis: "Reasoning about Functional Programs by Combining Interactive and Automatic Proofs"
Director Académico: Dr. Alberto Pardo (Instituto de Computación, Facultad de Ingeniería, UdelaR / PEDECIBA Informática)
Directores de Tesis: Dra. Ana Bove y Dr. Peter Dybjer (Department of Computer Science and Engineering, Chalmers University of Technology, Göteborg, Sweden)
Tribunal:
- Dr. Daniel Fridlender (Facultad de Matemática, Astronomía y Física, Universidad Nacional de Córdoba, Argentina) - Revisor -
- Dr. Alexandre Miquel (Instituto de Matemática y Estadística, Facultad de Ingeniería, UdelaR) - Revisor -
- Dr. Mauro Jaskelioff (Facultad de Ciencias Exactas, Ingeniería y Agrimensura, Universidad Nacional de Rosario, Argentina)
- Dra. Nora Szasz (Facultad de Ingeniería, Universidad ORT Uruguay / PEDECIBA Informática)
- Dr. Gustavo Betarte (Instituto de Computación, Facultad de Ingeniería, UdelaR / PEDECIBA Informática)
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.