Total Haskell is Reasonable Coq

Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich
11/25/2017
cs.PL

Official code: antalsz/hs-to-coq (283 stars, MIT, last commit 2020-11-11).

Abstract

We would like to use the Coq proof assistant to mechanically verify properties of Haskell programs. To that end, we present a tool, named hs-to-coq, that translates total Haskell programs into Coq programs via a shallow embedding. We apply our tool in three case studies -- a lawful Monad instance, "Hutton's razor", and an existing data structure library -- and prove their correctness. These examples show that this approach is viable: both that hs-to-coq applies to existing Haskell code, and that the output it produces is amenable to verification.

View on arXivView PDF

Code Implementations(1)

antalsz/hs-to-coqOfficial100%
MIT

Convert Haskell source code to Coq source code

28326C++, CoqMar 23, 20175 years agoMIT

Similar Papers

Harnessing Code Agents for Automatic Software Verification

80% match2026

Verified Low-Level Programming Embedded in F*

80% match1 repo5222017

Leveraging Large Language Models for Automated Proof Synthesis in Rust

79% match2023

Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification

78% match1 repo312024

Trustworthy Formal Natural Language Specifications

78% match2023

AutoVerus: Automated Proof Generation for Rust Code

78% match2024

Cite this paper

@article{spectorzabusky2017total,
  title  = {Total Haskell is Reasonable Coq},
  author = {Antal Spector-Zabusky and Joachim Breitner and Christine Rizkallah and Stephanie Weirich},
  year   = {2017},
  eprint = {1711.09286},
  archivePrefix = {arXiv},
  url    = {https://arxiv.org/abs/1711.09286}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/1711.09286.svg)](https://codeofpaper.com/paper/1711.09286)

Discussion