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

Talks

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