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 mailto: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 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_pro... 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.