We’ve started a podcast! @awsto.bsky.social and @samps.phd host “Current Continuation,” a little interview series with PL researchers. The first two episodes are with @ranjitjhala.bsky.social and @satnam6502.bsky.social. sigplan.org/cc/
the latest SIGPLAN blog post is front page on HN:
blog.sigplan.org/2025/08/29/a...
In this episode of Current Continuation, Adrian Sampson and I talk to Prof. Sarah E. Chasins of UC Berkeley. Sarah does awesome work at the intersection of PL, HCI, and social science! Enjoy!
www.youtube.com/watch?v=9NPI...
🚀 Announcing QECLean, our effort to formalize quantum error correction and fault-tolerance in Lean. The effort is led by PhD student, Stavan Jain.
We have a full formalization of the Toric Code and a proof of its distance, [[2L^2, 2, L]]! And more to come...
Here's a paper describing quantum computing using standard programming constructs, w/o the linear algebra!
The hope is that this will demystify quantum computing and serve as a formal foundation for reasoning about quantum programs.
paper eprint.iacr.org/2025/1091.pdf
code github.com/qqq-wisc/qwla
LSU is using this in their quantum computing course: arxiv.org/pdf/2511.02844
"Students begin with ... QWLA, a lightweight simulation framework that supports intuitive engagement with core quantum ideas without requiring prior knowledge of matrix algebra."
