I am interested in research on programming languages and streaming systems; I am particularly interested in using formal methods to verify real-time controllers, such as the controllers that are present in autonomous vehicles. Streaming languages are particularly well-suited to implementing real-time controllers as both have strict bounds on memory and compute time, but I have also previously worked on applying streaming languages to machine-learning workloads.
I am currently actively working on:
- Pipit, an embedded language for implementing and verifying reactive systems, which is implemented and partially verified in the F* theorem prover;
- Wyvern, a programming language with effect and capability tracking, so that one gets certain security properties by default.
I have previously worked on projects such as: