A formalization of GHC’s core language

There have been a handful of papers about System FC, the internal language used within GHC ([1] [2] [3] [4], etc.). Each of these papers uses a different characterization of FC, with variations among the definitions and judgments. Unsurprisingly, each of these formalisms differs also from the actual implementation of FC within GHC. At ICFP, Simon PJ asked me to look at GHC’s implementation of System FC, and write it up using formal notation. The result of this work (developed using Ott) now lives in the GHC repo, in docs/core-spec. There are comments in various places reminding GHC contributors to update the formalization as they update the implementation.

Do you have a stake in this work? Are you planning on reasoning about GHC’s core language? Check out the formalism here. Any feedback is welcome!


7 thoughts on “A formalization of GHC’s core language

    1. Richard Eisenberg Post author

      If by “write this up”, you mean [try to] publish a paper, then no. It took me maybe a total of 10-12 hours to produce the document, and I don’t think there’s anything inherently interesting enough in it to be publishable. By all means correct me if you think I’m wrong! In the meantime, please use it in your work.

    1. Richard Eisenberg Post author

      The document is essentially a transliteration of the code already in GHC. The typing rules are straight from the code in coreSyn/CoreLint.lhs. There is no analogous implementation of any operational semantics in GHC. Of course, to get much mileage from the rules I’ve written down, one would need some sort of semantics, but I think that properly belongs elsewhere. Another explicit goal of this exercise was to make this document maintainable by contributors to GHC, and adding operational semantics with no direct attachment to a chunk of code seemed to go against this goal.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s