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=com... 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_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.