On 2017-12-18 11:08 AM, Richard Eisenberg wrote:
… formalizing a variant is already underway. See https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1076&context=compsci_pubs
for a recent paper discussing (among other things) a formalization
of a dependently-typed version of Core. Much more development in
the formalization has taken place since that paper was written,
but you’ll have to contact Stephanie Weirich (sweirich@cis.upenn.edu) for the
latest, as I’m not involved at the ground level of the
formalization.
The past two issues of Haskell Weekly News have
mentioned research from some of the same people:
Total
Haskell is reasonable Coq
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.
Finding
bugs in Haskell code by proving it
We have used hs-to-coq on various examples, as described in our
CPP’18 paper, but it is high-time to use it for real.