Interesting read I had while trying to understand how much ECS systems have been explored by Type Theory / PL people. It’s surprisingly approachable aside from a few proofs which went over my head. Tracked down the published paper off of arxiv, you can find it here: https://dl.acm.org/doi/10.1145/3763050