Diagramming Program Values by Spatial Refinement
@ PLDI
Siddhartha Prasad
I am a PhD student in Computer Science at Brown, advised by Shriram Krishnamurthi. I work in programming languages and formal methods, with a focus on the gap between what people mean and what computational systems do.
My time as a software engineer1 taught me that programming is not just the mechanical task of writing code; it is also the cognitive work of formalization and judgment. Whether you are a professional programmer or someone newly empowered by GenAI, you still have to decide what the system should do, evaluate tradeoffs, and determine whether the result is fit for purpose. Too many formal tools treat the specification as an input that has already been settled, rather than something programmers discover and revise through the process of building. I am interested in how programming languages and formal methods can support this cognitive work as it happens, rather than entering only after the hard decisions have already been made. My research repurposes formal machinery traditionally aimed at automated analysis to support human understanding.
📣 On the job market. I am seeking academic and research positions for 2027–28. Get in touch.
Current Projects
Making diagrams as cheap as printf.
Every time you inspect a value (at the REPL, in a debugger, in a print statement) you should have the option of seeing a diagram. Read the Spytial blog post →Checking what GenAI wrote, meaningfully.
When an LLM generates a regex for you, how do you know it's the one you actually needed? Read the regex post → Or how it generalizes to more languages →Understanding how humans understand Temporal Logic.
I think of human misconceptions as alternate semantics for the logic. Read about LTL and LTLf misconceptions → Try the LTL Tutor to see how we operationalize misconceptions →-
At Microsoft, I worked on Windows’ XAML UI Framework from 2016-2018. I then worked on Azure’s AI services, with a particular focus on containerizing AI, from 2018-2021. ↩