Amos Robinson

Postdoctoral fellow


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:

  • 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.

You are on Aboriginal land.

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

bars search times arrow-up