[Haskell-cafe] The Definition of Haskell

[Richard Eisenberg]

> On Dec 18, 2017, at 12:27 PM, Todd Wilson <twilson at csufresno.edu> wrote:
> 
>  It looks like formalizing and proving safety for this system in a proof assistant would make a good project.

It would, but 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) for the latest, as I’m not involved at the ground level of the formalization.

Richard
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20171218/a667c42a/attachment.html>