Thesis project: formalisation of Icicle in Isabelle or Coq

[amosr]

Icicle[1] is a streaming query language that uses a type system to ensure that queries can be executed in a single-pass over the input stream with no buffering, and that any two queries over the same input stream can be executed together.

This project would involve formalising the type system and the evaluation semantics of Icicle in an interactive theorem prover, such as Isabelle or Coq.

--- TODO: I don't have a good enough grasp on how big this project is. I'll have to think about it a bit more to figure out what's involved.

[1] https://www.cse.unsw.edu.au/~amosr/papers/robinson2016icicle.pdf