Lightnews — Scholar-powered news

Sam Westrick @shwestrick.bsky.social · 28m

Mizuki Arata presents LunarML — an impressive implementation!! It compiles standard ML down to either Lua or JavaScript. Tons of features. Check it out! github.com/minoki/LunarML

Sam Westrick @shwestrick.bsky.social · 2h

John presents new compiler optimization work inside of SML/NJ —

Sam Westrick @shwestrick.bsky.social · 3h

Dave is up! Calling in all the way from the Oregon coast

1

Sam Westrick @shwestrick.bsky.social · 3h

you can follow the live feed here:

www.youtube.com/live/8B4VrU_...

1 1

Sam Westrick @shwestrick.bsky.social · 5h

See you there!!
conf.researchr.org/home/icfp-sp...

ML Family Workshop 2025 - Higher-order, Typed, Inferred, Strict: ML Family Workshop 2025 - ICFP/SPLASH 2025

ML is a large family of programming languages that includes Standard ML, OCaml, F#, CakeML, SML#, Manticore, MetaOCaml, JoCaml, Alice ML, Dependent ML, Flow Caml, Reason ML, Flix, MaPLe, and many othe...

conf.researchr.org

Sam Westrick @shwestrick.bsky.social · 5h

finally, to close the day, we have Samuel Vivien, Yanni Lefki, and Martin Elsman

1

Sam Westrick @shwestrick.bsky.social · 5h

next up, right after lunch, we have Wenhao Tang, Viviana Bono, and Yong Kiam Tan

1

Sam Westrick @shwestrick.bsky.social · 5h

in the first session, presentations from Dave MacQueen, John Reppy, and Mizuki Arata

1

Sam Westrick @shwestrick.bsky.social · 5h

the ML Family Workshop begins in just a few hours! Come find us in Peony NE at 10:30, right next to the dining hall

We have a great program with 9 talks!

If you are curious about compilers, type systems, module systems, formal proofs, and typed domain modeling, then this is the place for you

1 1 3

Sam Westrick @shwestrick.bsky.social · 12d

We got really fantastic feedback during reviews (thank you POPL reviewers!) and we're looking forward to updating this preprint. Stay tuned for the final paper

Sam Westrick @shwestrick.bsky.social · 12d

Of course, there are tons of juicy details and intricacies that cannot fit into (even this many) tweets. Take a look at the preprint to see all the nitty gritty stuff!

cs.nyu.edu/~am15509/pub...

cs.nyu.edu

1

Sam Westrick @shwestrick.bsky.social · 12d

One of the surprising things we discovered is that this "backwards-in-time" / "up-pointer invariant" concept can be very elegantly encoded in the type system as a form of subtyping that we call subtiming.

The whole system is essentially just standard unification + subtiming

⬇️

1

Sam Westrick @shwestrick.bsky.social · 12d

thinking about a tree of tasks (where parents fork into their children), this corresponds to an **up-pointer invariant**: the data of child tasks can only contain pointers to ancestor data.

In this way, you can never have pointers between concurrent siblings/cousins/etc

⬇️

1

Sam Westrick @shwestrick.bsky.social · 12d

at compile-time, TypeDis computes a partial order over timestamps (derived from the nested fork-join structure of parallel tasks) and enforces that all pointers must flow _backwards_ in time

⬇️

1

Sam Westrick @shwestrick.bsky.social · 12d

Yes! enter TypeDis

similar to region types, TypeDis associates a task identifier or "timestamp", δ, with every allocation.

e.g. the type string@δ indicates that the string was allocated at time δ

Unboxed types don't need these annotations (e.g. raw integers, booleans, etc)

⬇️

1

Sam Westrick @shwestrick.bsky.social · 12d

Can we reason about disentanglement _statically_, at the source level, and enforce it automatically at compile-time?

In other words: can we statically guarantee that the GC remains fully parallel, and never has to synchronize across concurrent tasks??

⬇️

1

Sam Westrick @shwestrick.bsky.social · 12d

Nearly-zero cost only holds if your program is disentangled; as soon as a violation is detected, the GC has to start synchronizing across concurrent tasks and we're back to the tricky world of reasoning about the synchronization overheads of GC

So, the question is... ⬇️

1

Sam Westrick @shwestrick.bsky.social · 12d

today, in MaPLe, disentanglement is checked and managed dynamically

We've put a ton of work into ensuring that this dynamic management cost is nearly zero (see dl.acm.org/doi/10.1145/... and dl.acm.org/doi/10.1145/...)

However, ⬇️

1

Sam Westrick @shwestrick.bsky.social · 12d

The idea is (1) give every task its own local heap, and (2) enforce that the heaps of any two _concurrent_ tasks never directly point to each other, i.e., the heaps are "disentangled"

We've been exploring this idea over the past ~10 years in MaPLe (github.com/mpllang/mpl)

GitHub - MPLLang/mpl: The MaPLe compiler: efficient and scalable parallel functional programming

The MaPLe compiler: efficient and scalable parallel functional programming - MPLLang/mpl

github.com

1

Sam Westrick @shwestrick.bsky.social · 12d

Disentanglement is all about parallel GC. It decomposes the heap into pieces that can be traced independently, in parallel, with no synchronization

How does it work?

1

Sam Westrick @shwestrick.bsky.social · 12d

in TypeDis (conditionally accepted at POPL!), we develop a type system for enforcing **disentanglement** statically at compile-time. This project was led by Alexandre Moine here at NYU, in close collaboration with Stephanie Balzer at CMU.

Sam Westrick @shwestrick.bsky.social · 12d

absolutely thrilled to announce 2 papers (conditionally) accepted at POPL!

TypeDis: A Type System for Disentanglement
(Moine, Balzer, Xu, Westrick)

All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs
(Moine, Westrick, Tassarotti)

1 2

Reposted by Sam Westrick

Yaron Minsky @yminsky.bsky.social · 12d

Excited to say that we're looking to hire someone to focus on OxCaml education! We're doing enough to change the language that we have a pretty big internal education task ahead of us, and we want to hire someone to focus on it!

Please share this with others!

www.janestreet.com/join-jane-st...

OxCaml Educator :: Jane Street

Jane Street is a quantitative trading firm and liquidity provider with a unique focus on technology and collaborative problem solving.

www.janestreet.com

1 7 16

Reposted by Sam Westrick

Anil Madhavapeddy @anil.recoil.org · 12d

And if you’re interested in OxCaml, we have a tutorial on Sunday at ICFP walking through it conf.researchr.org/track/icfp-s... (materials will be online for anyone afterwards. Just the minor detail of finishing writing them first)

3 10

Sam Westrick @shwestrick.bsky.social · 12d

Both projects led by Alexandre Moine here at NYU.

Preprints available on Alexandre's website!
cs.nyu.edu/~am15509/

Home - Alexandre Moine

cs.nyu.edu

1

Sam Westrick @shwestrick.bsky.social · 12d

absolutely thrilled to announce 2 papers (conditionally) accepted at POPL!

TypeDis: A Type System for Disentanglement
(Moine, Balzer, Xu, Westrick)

All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs
(Moine, Westrick, Tassarotti)

1 7