About me
I am a computer science researcher at the Australian National University, where I work with Alex Potanin. I am interested in programming languages, streaming systems, and lightweight formal methods such as model-checking.
I am currently developing a programming language for implementing and verifying reactive systems, called Pipit; it is implemented and partially verified in the F* theorem prover. This work emerged from a previous project called Songlark, which is an unverified model-checker for reactive systems.
I previously worked at Ghost Locomotion where I applied formal methods to autonomous vehicles.
I have co-supervised some honours students related to Cogent, a programming language designed to reduce the cost of formal verification.
I previously worked at Ambiata, where I developed Icicle, a domain-specific language for efficient streaming queries over large data sets.
I undertook my PhD in the Programming Languages and Systems group at UNSW. My supervisors were Ben Lippmeier, Gabriele Keller and Manuel Chakravarty. My doctoral thesis was about streaming models and fusion for the efficient concurrent execution of multiple queries.
(github)
(mastodon)
(twitter)
(amos at songlark dot net)
Publications
Pipit on the Post: proving pre- and post-conditions of reactive systems (preprint). (github project)
Amos Robinson, Alex Potanin.
(in submission).
Pipit: reactive systems in F* (extended abstract). (github project)
Amos Robinson, Alex Potanin.
Type-driven Development (TyDe) 2023.
Smart contracts as authorized production rules. (Isabelle proofs) (github project)
Ben Lippmeier, Amos Robinson, Andrae Muys.
Principles and Practice of Declarative Programming 2019.
The stuff that streams are made of: Streaming models for concurrent execution of multiple queries.
Amos Robinson
Doctoral thesis 2018.Machine fusion: merging merges, more or less. (Coq proofs) (implementation)
Amos Robinson, Ben Lippmeier.
Principles and Practice of Declarative Programming 2017.Icicle: write once, run once. (implementation)
Amos Robinson, Ben Lippmeier, Gabriele Keller.
Functional High Performance Computing 2016.Polarized data parallel data flow. Ben Lippmeier, Amos Robinson, Fil Mackay.
Functional High Performance Computing 2016.Fusing filters with integer linear programming. (video) (slides) (errata)
Amos Robinson, Ben Lippmeier, Gabriele Keller.
Functional High Performance Computing 2014.Data flow fusion with series expressions in Haskell.
Ben Lippmeier, Manuel Chakravarty, Gabriele Keller, Amos Robinson.
Haskell Symposium 2013.Rewrite rules for the Disciplined Disciple Compiler.
Honours thesis at UNSW.
Talks
Applicative invariants for Lustre
2022/11/27. Synchron22 workshop, France (preliminary research talk)Model-checking techniques for reactive systems
2022/08/17. FP-Syd (literature review talk)Pretending to verify a train controller with Lustre
2020/03/22. FP-SydRust without monads: Hedgehog-style property-based testing without the noise
2020/02/01. FP-Syd workshopHow to win your first Coq fight (extra material)
2018/05/23. FP-SydMachine fusion: merging merges, more or less
2017/09/20. Principles and Practice of Declarative Programming (resarch talk)Icicle: write once, run once (video)
2016 Lambda Jam, Brisbane. (research talk)Fusing filters with integer linear programming (video)
2014 FHPC Gothenburg (research talk)
Projects
Songlark
Songlark is an embedded domain-specific language for model-checking reactive control systems. The idea is that by using an embedded language, we can use a simpler core language and get some features "for free".
Songlark combines existing research techniques with some new research. It is currently in an early experimental stage.
Folderol: stream fusion for multiple queries or consumers
Folderol is an implementation of Machine fusion for fusing and executing concurrent streaming queries. Combinators in a streaming program are represented as processes in a Kahn process network. We keep the determinism of list and streaming programs, while being able to coordinating between multiple consumers, which is necessary for executing multiple queries. This project uses Template Haskell to construct process networks and generate fused processes at compile-time.
This project is a combination of conceptual work on a novel fusion system and low-level implementation details for generation of efficient code.
Icicle: a streaming query language
When dealing with large data sets that do not fit in memory, it is crucial to limit the number of accesses and iterations over the data set. However, in a high level language it may not be immediately obvious how many iterations a particular program will require. The number of iterations becomes even less obvious in the presence of heuristic and statistics-based optimisations, as used by traditional databases: a small tweak to the query or even modifying the number of rows in a table can cause drastic changes to the query plan.
As data sets continue to grow, a high level language with predictable runtime characteristics becomes more necessary. Programmers should not need to understand the internal workings of a database or query optimiser in order to write fast queries.
At Ambiata, we have designed and implemented Icicle, a query language specifically for single-pass queries. This means that any query in our language is assured to compile into a single iteration over the data set. We use a type system based on temporal logic to ensure that queries can be executed in a single pass without violating causality. Queries are then compiled to a stream-based intermediate language, which allows multiple queries to be merged together, removing duplicate computations. Finally, queries are compiled to high-performance C code.
Clustering
Finding the best fusion clustering is actually NP-hard (as proved by Alain Darte). By converting combinator programs to integer linear programs, we can generally find good clusterings in adequate time.
Disciplined Disciple Compiler (DDC)
DDC is a research compiler for a strict functional language with effect typing. It isn’t particularly useful yet, but has some interesting optimisations.
Linear Integer/Mixed Programming (LIMP)
A fairly simple Haskell library for expressing linear programs. At the moment, there’s only a simplifier, COIN/CBC bindings, and pretty-printing.
Students
Vivian Dang (honours 2020, co-supervised with Christine Rizkallah)
Information-Flow Security for CogentAlex Hodges (honours 2019, co-supervised with Christine Rizkallah)
Property Based Testing of C Code from Haskell