[Haskell-cafe] The Definition of Haskell

Richard Eisenberg rae at cs.brynmawr.edu
Mon Dec 18 18:08:13 UTC 2017

> 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.

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

More information about the Haskell-Cafe mailing list