I am excited to announce that our paper "Back to Direct Style: Typed and Tight" has been accepted at OOPSLA'23.

We present a typed translation, which allows compilers to go to CPS, perform optimizations, and go back to direct-style (DS).

The translation...
- preserves well-typedness
- preserves semantics
- is a syntactic right-inverse of the CPS translation (that is, going to CPS and back is the identity)
- it is a left-inverse of the CPS translation, if DS programs don't use control effects


@hazel According to the discussion it looks like their server is banned for bad behavior. So I guess that is a no

Show thread

@hazel hey, Gabriele and I tried to connect here, but there seems to be a problem with a block. Anything we can do there, or is it not possible to connect with people on that particular instance?

Thanks :)


I am excited to see our OOPSLA artifact being selected for the "Distinguished Artifact Award"!

If you want to play around with our implementation or browse our Coq proofs, you can find it here:

Gentle reminder: We have openings for an assistant/associate professor in software engineering in Delft! Wonderful team, amazing students, and lots of opportunities to work with societal and industry partners. Apply now, deadline November 27! tudelft.nl/over-tu-delft/werke

#SoftwareEngineering #Hiring #vacancy #professor #tudelft @seresearchers


A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.