Looking for recent works on STG

[Sebastian Graf]

Addendum: This is what I mean by Sestoft-style:
http://www.itu.dk/~sestoft/papers/amlazy.pdf
This describes the simplest possible small-step transition semantics for
call-by-need (discounting ADTs).
If you don't care about all the transitions, it might be simpler to switch
to a *contextual* semantics instead, which express stack, heap and
environment simply as an evaluation context. Then you might want to look at
this work by Ariola et al.: https://dl.acm.org/doi/10.1145/199448.19950,
who first figured out what the evaluation contexts for call-by-need are.
The advantage of contextual semantics is that you need far fewer "search
transitions" that just push stack frames or add heap bindings to find the
next redex.
This style harmonises well with proofs by induction on evaluation contexts,
which you often do to show program equivalence.

Am So., 26. Mai 2024 um 14:18 Uhr schrieb Sebastian Graf <
sgraf1337 at gmail.com>:

> 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.
> I did that for example in my denotational interpreter for Core here
> <https://gitlab.haskell.org/ghc/ghc/-/blob/64ae8fff5239b7c2c58692ce3b0e03f63f01bca1/compiler/GHC/Core/Semantics.hs#L161>,
> generating a trace in a Sestoft-style small-step operational semantics.
> It works quite well (until it encounters an import or a primop which I
> haven't implemented), see here
> <https://mastodon.online/@sgraf/111715016532134390>.
> 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
> <https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/eval-apply.pdf>,
> 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
>
> Am So., 26. Mai 2024 um 14:03 Uhr schrieb Moritz Angermann <
> moritz.angermann at gmail.com>:
>
>> 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.
>>
>> On Sun, 26 May 2024 at 7:40 PM, Rodrigo Mesquita <
>> rodrigo.m.mesquita at gmail.com> wrote:
>>
>>> Dear all,
>>>
>>> Do you know of any recent works on the STG?
>>>
>>> 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.
>>>
>>> Nonetheless, I’m also interested in possibly more recent formulations of
>>> STG (e.g. a mechanized one?) beyond the original paper.
>>>
>>> Cheers
>>> Rodrigo Mesquita
>>> _______________________________________________
>>> ghc-devs mailing list
>>> ghc-devs at haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>>
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20240526/a56f91f6/attachment.html>