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!
Types and Kinds 
Nice work! Were you planning on writing this up somewhere? The HERMIT team, who use GHC Core as our primary subject language, could use this.
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.
Why no operational semantics?
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.
Have you seen Simon Winwood’s (now at Galois’) Core formalized in Twelf/LF ?
No, I haven’t. A quick search turned up only a dead link for this. Do you know where I can find it?
I think you should mail Simon directly. He’s here now http://corp.galois.com/simon-winwood/