Want safe parallelism without compromising the simplicity of the lambda calculus?
𝜆∨ integrates an old idea (values can evolve over time according to a partial order) while also adding one new parallel composition operator and some spiffy streamable data types to achieve this.
Determinism, purity, and compositionality remain. Together, recursion and parallel composition let us express computations in interesting new ways!
My PLDI 2025 paper with Steve Zdancewic has the details!
📄Functional Meaning for Parallel Streaming
🔗arxiv.org/abs/2504.02975
Haven't heard this articulated enough, but glad I'm not alone in thinking of bidirectional type checking as a useful and easy to implement trick, but not a particularly deep one.
It falls down in so many situations. In addition to those in the QT'd thread, a while back I was frustrated by a situation in which it turns out bidirectional type checking is not preserved by eta expansion!
"Book" techniques should be robust under extension. But bidirectional type checking strikes me as flimsy. IMO it feels arbitrary as well. Eg there are multiple ways to synthesize/check function application with no answer that is always "right". i.cs.hku.hk/~bruno/papers/ar…
The recording of my HOPE talk "Granite: Compositional Functional Logic Programming" is now on YouTube!
youtu.be/siLJ1Z_vqj8?si=0FG2…
We were super lucky yesterday to have @arntzenius come out to Philly to chat with PL Club and speak about incremental programming, automatic differentiation, and bidirectional programming!
If you're at POPL and have the chance to grab lunch outside of the conference on a week day, I highly recommend checking out Chacarero for some really awesome Chilean sandwiches! It's a 15 minute walk from Park Plaza.
For an easy breakfast, Mike and Patty's is fantastic and less than 5 minutes from the conference! I think I owe @mkolosick for introducing me to their "Breakfast Grilled Crack" back in our Boston days.
PLTwitter, which papers/books/etc would you recommend to someone with a background in CS who is interested in PL and especially compilers?
They're interested in learning more about the area but not necessarily doing research.
Already recommended @jeanqasaur's PLTalk recordings.
I have never been so thoroughly destroyed in something as I was the day I for some reason thought it would be fun to play @ChrisKreider in badminton.
Nick Rioux retweeted
If you're surprised about the log4j vulnerability, just wait until you hear what happens when you put a java.net.URL into a hashtable
Nothing makes me feel at home quite like blasting Dirty Water after a Red Sox extra innings postseason win.
Hot take? Parsing is a hugely unsolved problem. We're getting there though.
There's a chicken and egg problem. Today's parsers solve existing use cases because systems that would require more can't even get off the ground. This in turn makes parsing research hard to motivate.
If you write LaTeX in Emacs and don't have pdf-tools (the 'pdf' layer in spacemacs) you are really missing out.
Tired: Types are sets of values
Wired: Girard mixed up ⊤ and ⊥, we have been subtyping negative types backwards for decades, and intersection types are a lie