Dan Plyukhin

If you always wanted to learn about the semantics of languages like Choral and HasChor, look no further! dplyukhin.github.io/files/relax-...

Highlights:

(1) Past models need dozens of rules to explain the semantics. Ours has ten.

(2) We give laws to help you design the right semantics. The laws work: we found three bugs in previous versions of Chorλ.

(3) Ours is similar to non-strict calculi, but with a "choreographic" flavor.

Choreographic λ-calculi are a hot topic. You might know models like Pirouette (POPL 2022) or Chorλ (ICTAC 2022).

But did you know researchers don't agree what the "right" semantics should even be?

Our ICFP pearl builds a tiny calculus from scratch, and shows the right semantics is... non-strict!?

Hey CS instructors and TAs, what’s your policy on students using LLMs?

(A) not allowed
(B) sometimes allowed
(C) required or encouraged

I think so too! A few interesting research problems to solve before it’s ready for production though, eg, rethinking some akka/pekko APIs to work well with actor GC

Ikr! I bet you could find ideas in forums, but I spoke to Jonas Bonér and he never mentioned any projects on that front. Maybe because fault recovery comes across as an intractably hard problem?

The title is "CRGC: Fault-Recovering Actor GC in Apache Pekko". The authors are Dan Plyukhin (SDU), Gul Agha (UIUC), and Fabrizio Montesi (SDU)

I gave a talk at PLDI '25 about the future of Actor GC in Apache Pekko - with applications to #akka #erlang and #elixir. It's the culmination of my 6+ year PhD at UIUC, and I tried to make the talk really fun and easy to follow :)

Check it out here: www.youtube.com/live/lGM37Z3...

[PLDI'25] Cosmos, Violet & Tulip - PLDI Research Papers (Jun 20th) YouTube video by ACM SIGPLAN

If you're reading this post, you're probably procrastinating. Why not watch my PLDI talk, "CRGC: Fault-Recovering Actor GC in Apache Pekko"?

It goes live in 1 hr (11:30 KST). I tried to make it entertaining 🙂

#akka #erlang #elixir www.youtube.com/live/lGM37Z3...

For the record I agree that state sponsored killing is wrong in any context, but not for the reason you cited. The joke tries to get at why I think the logic in the post is a bit twisted

If there are crimes for which death is too extreme a sentence, and crimes for which it is not extreme enough, by the intermediate value theorem aren’t there crimes for which it’s appropriate? /s

A decent employee (me) sabotaged by an awful manager (also me)

Sometimes it takes me all day to get nothing done

typedef struct { /* * Data mainly modified when someone is listing * the content of the table. */ union { ErtsPTabListData data; char algn[ERTS_ALC_CACHE_LINE_ALIGN_SIZE(sizeof(ErtsPTabListData))]; } list;

Under the hood, #Erlang does a lot of tricks to improve performance.

The fields of this C struct are modified by different CPUs. If you packed fields normally, modifications by one CPU will invalidate the cache of another CPU.

So the devs added padding, and now fields are on different cache lines!

Haskell could almost compete with Racket for language-oriented programming, but the current interface for monads is impossible to use without first learning the Haskell metalanguage

TIL monads give you some compiler optimizations for free!

E.g. gcc has the semantics of assignment built-in, so it optimizes away `int y = x; x = y; ...`.

If you write it in Haskell with the State monad, GHC will delete that code using beta/eta reduction. Even though GHC doesn't know about State!

More like curing toothache by replacing your jaw with a cool robot jaw that doubles as a pencil sharpener!

But seriously, does this mean you prefer deep embeddings over mixed embeddings for (say) a simple imperative language? I’m new to this whole conversation :p

Time to rewatch :) Adam is so great at showing what’s interesting about music theory while acknowledging its limitations

I find Moggi’s early papers about monads confusing. It’s hard to tell what exactly he was envisioning.

This paper does a great job filling in the gaps for a modern audience! Monads + dependent types are such a powerful way to define PLs and prove properties about them.

dl.acm.org/doi/pdf/10.1...

There’s a lot of parallels b/w Category Theory and Music Theory!

1) It’s descriptive, not prescriptive
2) You don’t need it to do good work but many find it useful
3) It’s easy to say “people who know more than me are snobs, people who know less are fools”
4) Novices use it to discredit other areas

This essay about feminism in PL asks some really tough questions!

It’s making me wonder: what should the purpose of PL research be, anyway?? Are we trying to “solve problems”, “make the world a better place”, “expand knowledge”, or…?

www.felienne.com/wp-content/u...

I don't think DOGE could cut budgets at this pace without the help of LLMs. Is this the first time AI has been used to accelerate a political project? Reminds me of what the invention of machine guns did to the first world war.

Love it but the docstring in cursive is cursed

Not only do I have word wrapping - I also use a sans serif font 💀

I have a copy of "Smalltalk 80: Bits of history, words of advice" and it's so refreshing to learn about the problems they were trying to solve back then

Idea to create a rival podcast to Type Theory Forall, focusing on untyped programming languages like lisp and prolog

It would be called "Judgment Free Zone" and the logo would obviously be (⊬)

Add a level of indirection! (Make a wrapper)

Right, that’s a fair criticism and worth discussing. But the comments I’m referring to just say “fuck you” without engaging with the concept. I’m guessing people have that emotional reaction because they feel their jobs are threatened or they’ve personally been burned by LLMs in higher ed somehow?

omg. If I got those comments I would leave the planet. I still don’t understand how the product deserves such vitriol. What collective nerve got triggered here?

Funny enough, this would mean CS programs have to start grading more like the humanities! Maybe adding more emphasis on ethics and design than ever before? An exciting prospect :)

Absolutely. I think this is a good opportunity to assign more student-directed projects. E.g. in a compilers course, instead of everyone implementing the same language, students design and implement their own.

+ Students more fulfilled
+ Students use LLMs to automate drudgery
- Harder to grade