Re: [Haskell-cafe] The Definition of Haskell

On Dec 18, 2017, at 12:27 PM, Todd Wilson 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@cis.upenn.edu) for the latest, as I’m not involved at the ground level of the formalization. Richard