Amos Robinson

Interests

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.

Projects

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:

• Songlark, an SMT-based model-checker for reactive systems - Songlark is the spiritual predecessor to Pipit mentioned above;
• Cogent, a programming language for verifying systems programs;
• Icicle, a streaming language for querying “big data” datasets.