We will no longer update the code here. All issues and pull requests should be reported on the repo.
hs-to-coq
Join our discussion on:
This repository contains a converter from Haskell code to equivalent
Coq code, as part of the CoreSpec component of the DeepSpec
project.
CPP'18 paper “Total Haskell is Reasonable
Coq” by Antal Spector-Zabusky,
Joachim Breitner, Christine Rizkallah, and Stephanie Weirich. This
paper describes the following examples:
bag Multiset implementation from GHC's implemention
The recommended way of building hs-to-coq is to use stack. If you have not
setup stack before, run:
stack setup
To build hs-to-coq, then run
stack build
(hs-to-coq can be built with GHC 8.4, 8.6, 8.8, and 8.10. However, the repo
only contains the translation of Haskell libraries such as base from GHC
8.4. Therefore, it is advised to build hs-to-coq with GHC 8.4 if you plan to
use example translations contained in this repo.)
Building the base library
This repository comes with a version of (parts of the) Haskell base library
converted to Coq, which you will likely need if you want to verify Haskell
code.
You must have Coq 8.10.2 and ssreflect to build the base library. To
install these tools:
opam repo add coq-released https://coq.inria.fr/opam/released (for
SSReflect and MathComp)
Coq has a single namespace for types and values hence the type name
will conflict with constructor name. One can pass -e edit file
containing custom directives to ensure correctness of generated code
with the following directive:
rename value Foo.SomeType = Foo.MkSomeType
See the manual for documentation
for the edits files.
Other directories
The examples/ directories contains a number of example translation and
verification projects, including
structural-isomorphism-plugin: (In progress.) A GHC plugin that connects
the re-extracted converted code back into GHC, allowing us to run Haskell
programs against verified/verifiable code. Currently does not work.
请发表评论