[Haskell-cafe] The Definition of Haskell

[Neil Mayhew]

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 at cis.upenn.edu
> <mailto:sweirich at 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 <https://haskellweekly.news/>
have mentioned research from some of the same people:

Total Haskell is reasonable Coq <https://arxiv.org/abs/1711.09286>

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
<https://www.joachim-breitner.de/blog/734-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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20171218/59c56167/attachment.html>