Compiling Haskell into Lean: A Common Abstract Syntax for Haskell and Interactive Theorem Provers

<p>In this work, we introduce a program conversion tool, HS-TO-LEAN, that uses GHC's <em>ghc-lib-parser</em> API to translate Haskell programs into Lean code, which is then validated by the Lean compiler. The repo can be found at https://github.com/holcombet/hs-to-lean/tree/main. The result is a successful compilation of a fragment of Haskell into correct and executable Lean code that users can prove theorems about. We conducted a case study using a heap sort algorithm to support our claim that HS-TO-LEAN produces verifiable Lean code. Our approach is inspired by recent advances in formal verification of Haskell programs in Coq, and we currently restrict our attention to total Haskell.</p> <p>The compiler produces an AST that serves as a common level of abstraction between a fragment of Haskell and Lean. The abstract common fragment promotes translation between languages by simplifying and restructuring GHC's original AST, improving the readability and linearization of the AST.</p> <p>Future work on HS-TO-LEAN will extend the compiler to translate to other interactive theorem provers, including Coq, Agda, and Isabelle, making it portable and accessible to a range of verification efforts and communities. Future work also includes implementing bidirectionality, supporting the translation of Haskell code to a target proof assistant and vice versa. This method will expose an interesting level of abstraction that is applicable to all of the languages involved and produce a more maintainable compiler.</p> <p>These results contribute to the ongoing work in the formalization and verification of mathematics and programming and present a viable approach to unifying the formal systems of different proof assistants.</p>

Level thesis:degree_level

Thesis

Discipline thesis:degree_discipline

Electrical Engineering and Computer Science

Year

2025

Author dc:creator

• Holcombe, Talitha

Contributors dc:contributor

• Dr. Alexander Kurz
• Dr. Jonathan Weinberger
• Dr. Andrew Moshier

• Lean
• formal verification
• program verification
• Programming Languages and Compilers

Repository record dc:identifier

https://digitalcommons.chapman.edu/eecs_theses/3

OAI identifier oai:identifier

oai:digitalcommons.chapman.edu:eecs_theses-1003