Hey Rodrigo,
With any kind of semantics, often the most important question is: What do you want to achieve with it?
Generally speaking, I think it would be tedious, but not all that hard, to define an STG-style semantics for Core that "simply" anfises on the fly.
It works quite well (until it encounters an import or a primop which I haven't implemented), see
here.
If you really insist on modelling the STG machine (the prime advantage of which is that it can be efficiently compiled to hardware), then you would need to figure out the manifest arity of functions before you put them in the heap, etc..
But even that should not be hard, taking the STG operational semantics from the
eval/apply paper, which should be amenable to mechanised formalisation. It's still tedious unless you really need to observe some STG-specific detail in your work.
So yeah, what is your end goal here?
Cheers,
Sebastian