Last month saw the 43rd edition of the ACM SIGPLAN-SIGACT Symposium on the Principles of Programming Languages (POPL). Gabriel Scherer did a wonderful job of gathering links to all of the accepted papers in a GitHub repo. For this week, I’ve chosen five papers from the conference that caught my eye.

Links will go live as the week progresses.

• PSync: a partially synchronous language for fault-tolerant distributed algorithms is an embeddable DSL for distributed algorithms that also supports automated formal verification.
• If you don’t really understand what your hardware does, that makes it very hard to reason about the correctness of programs that run on of it. In Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA we get a look into the complexities of a modern processor, and the first formal specification of ARMv8 semantics.
• ‘Cause I’m Strong Enough: Reasoning About Consistency Choices in Distributed Systems introduces ‘The Rule.’ How do you know that your data integrity invariants will not be violated? Use The Rule to prove it…
• Last month we saw how intricate recovery can be. Which makes it all the more impressive that, in the context of filesystem operations, Reducing Crash Recoverability to Reachability shows that it is possible to analyze real C code and automatically prove whether or not it is crash-recoverable. Clever stuff!
• Gradual Typing sounds like a great idea, but Is Sound Gradual Typing Dead?. Will we ever be able to make it perform well enough to be acceptable?