<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
On 2017-12-18 11:08 AM, Richard Eisenberg wrote:<br>
<blockquote type="cite"
cite="mid:86FAC343-5192-42CA-9D42-4C01250873B3@cs.brynmawr.edu">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
… formalizing a variant is already underway. See <a
href="https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1076&context=compsci_pubs"
class="" moz-do-not-send="true">https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1076&context=compsci_pubs</a>
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 (<a
href="mailto:sweirich@cis.upenn.edu" class=""
moz-do-not-send="true">sweirich@cis.upenn.edu</a>) for the
latest, as I’m not involved at the ground level of the
formalization.<br>
</blockquote>
<br>
The past two issues of <a moz-do-not-send="true"
href="https://haskellweekly.news/">Haskell Weekly News</a> have
mentioned research from some of the same people:<br>
<br>
<a moz-do-not-send="true" href="https://arxiv.org/abs/1711.09286">Total
Haskell is reasonable Coq</a><br>
<br>
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.<br>
<br>
<a moz-do-not-send="true"
href="https://www.joachim-breitner.de/blog/734-Finding_bugs_in_Haskell_code_by_proving_it">Finding
bugs in Haskell code by proving it</a><br>
<br>
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.<br>
</body>
</html>