HOL - ML - Haskell

Aims

The project aims to bridge the gap between programming and proving in the interactive proof assistant Isabelle/HOL by two major developments:

Working areas

Function package

The function package supports specification of recursive functions in Isabelle/HOL in a style very close to that of functional programming languages where the necessary termination proofs are often automatic. Mutual and nested recursion is also covered. Termination can be proved automatically in many cases.

Code generator

In Isabelle/HOL, code generation is understood as the transformation of a system of equational theorems into a program in a functional programming language with the same equational semantics. This guarantees partial correctness of generated programs.

This generic framework is instantiated for SML, OCaml and Haskell. The meta-theory permits program and datatype refinement, i.e. the replacement of abstract algorithms and representations by efficient and executable programs and data structures – without endangering partial correctness.

On top of this, the scope of executable specifications can be extended by providing tools which produce suitable equational specifications from theories. An example is a predicate compiler which turns inductive specifications into equational ones, thus opening the world of functional-logic programming for code generation.

Additionally, we have provided Haskabelle which transforms a subset of Haskell to Isabelle/HOL theory text.

Bibliography

[1]
Klaus Aehlig, Florian Haftmann, and Tobias Nipkow. A Compiled Implementation of Normalization by Evaluation. In Otmane Aït Mohamed, César Muñoz, and Sofiène Tahar, editors, TPHOLs '08: Proc. of the 21th International Conference on Theorem Proving in Higher Order Logics, volume 5170 of LNCS, pages 352-367. Springer, 2008.
[2]
Stefan Berghofer, Lukas Bulwahn, and Florian Haftmann. Turning inductive into equational specifications. In TPHOLs '09: Proc. of the 22th International Conference on Theorem Proving in Higher Order Logics, volume 5674 of LNCS. Springer, 2009.
[3]
Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkök, and John Matthews. Imperative Functional Programming with Isabelle/HOL. In Otmane Aït Mohamed, César Muñoz, and Sofiène Tahar, editors, TPHOLs '08: Proc. of the 21th International Conference on Theorem Proving in Higher Order Logics, volume 5170 of LNCS, pages 352-367. Springer, 2008.
[4]
Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow. Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL. In K. Schneider and J. Brandt, editors, Theorem Proving in Higher Order Logics (TPHOLs 2007), volume 4732 of LNCS, pages 38-53. Springer, 2007.
[5]
Florian Haftmann. From Higher-Order Logic to Haskell: There and Back Again. In John P. Gallagher and Janis Voigtländer, editors, Proceedings of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2010, Madrid, Spain, January 18-19, 2010. ACM Press, 2010.
[6]
Florian Haftmann. Code Generation from Specifications in Higher Order Logic. PhD thesis, Technische Universität München, 2009.
[7]
Florian Haftmann and Tobias Nipkow. Code Generation via Higher-Order Rewrite Systems. In Matthias Blume, Naoki Kobayashi, and Germán Vidal, editors, Functional and Logic Programming: 10th International Symposium: FLOPS 2010, volume 6009 of LNCS. Springer, 2010.
[8]
Alexander Krauss. Partial Recursive Functions in Higher-Order Logic. In Ulrich Furbach and Natarajan Shankar, editors, Automated Reasoning (IJCAR 2006), volume 4130 of LNCS, pages 589-603. Springer, 2006.
[9]
Alexander Krauss. Certified Size-Change Termination. In Frank Pfenning, editor, Automated Deduction (CADE-21), volume 4603 of LNCS, pages 460-476. Springer, 2007.
[10]
Alexander Krauss. Automating Recursive Definitions and Termination Proofs in Higher-Order Logic. PhD thesis, Technische Universität München, 2009.
[11]
Alexander Krauss. Partial and Nested Recursive Function Definitions in Higher-order Logic. J. Automated Reasoning, 44(4):303-336, 2010.