<div dir="ltr"><div>Hey Rodrigo,</div><div><br></div><div>With any kind of semantics, often the most important question is: What do you want to achieve with it?</div><div><br></div><div>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.</div><div>I did that for example in my <a href="https://gitlab.haskell.org/ghc/ghc/-/blob/64ae8fff5239b7c2c58692ce3b0e03f63f01bca1/compiler/GHC/Core/Semantics.hs#L161">denotational interpreter for Core here</a>, generating a trace in a Sestoft-style small-step operational semantics.</div><div>It works quite well (until it encounters an import or a primop which I haven't implemented), see <a href="https://mastodon.online/@sgraf/111715016532134390">here</a>.</div><div>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..<br></div><div>But even that should not be hard, taking the STG operational semantics from the <a href="https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/eval-apply.pdf">eval/apply paper</a>, which should be amenable to mechanised formalisation. It's still tedious unless you really need to observe some STG-specific detail in your work.</div><div><br></div><div>So yeah, what is your end goal here?</div><div><br></div><div>Cheers,</div><div>Sebastian<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Am So., 26. Mai 2024 um 14:03 Uhr schrieb Moritz Angermann <<a href="mailto:moritz.angermann@gmail.com">moritz.angermann@gmail.com</a>>:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="auto">I don’t know myself, but I would suggest reaching out to Csaba. I believe he might have a good grasp on the STG literature.</div><div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, 26 May 2024 at 7:40 PM, Rodrigo Mesquita <<a href="mailto:rodrigo.m.mesquita@gmail.com" target="_blank">rodrigo.m.mesquita@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Dear all,<br>
<br>
Do you know of any recent works on the STG?<br>
<br>
In particular, I am looking for a result connecting STG's execution and Core’s call-by-need semantics when written in structural operational semantics style.<br>
<br>
Nonetheless, I’m also interested in possibly more recent formulations of STG (e.g. a mechanized one?) beyond the original paper.<br>
<br>
Cheers<br>
Rodrigo Mesquita<br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div></div>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>