Type systems can provide static guarantees about the behaviour of all possible programs written in a language. This project involves the combination of two recent advances in type theory: graded and guarded modalities.
Graded modalities: Computation costs money, and writing programs that do more work than intended can be a major problem. For example cloud providers are notorious for sending surprisingly large bills to clients who underestimated the computational needs of their programs. Graded modalities are type formers that give programmers control over the cost of their programs, as well-typed programs can never do more work than the programmer is willing to allow.
Guarded modalities: Most type systems provide guarantees about the output of terminated runs of programs. This is not a meaningful notion for applications that are intended to run continually, producing outputs as they go. Instead of guarantees about a final output, we would instead like guarantees about ‘productivity’, which means that for as long as the program runs, it will continue to produce correct output. Guarded modalities are type formers that allow programmers to write non-terminating programs, but disallow such programs that are not productive.
This project seeks answers to the question: can types be used to specify the cost of non-terminating programs? This will involve the design of an idealised programming language, based on lambda calculus, with both graded and guarded modalities, in which the programmer may specify how much cost may be incurred for each additional step of the program. The student will show the correctness of their proposed system by means of an inductive mathematical proof, guaranteeing that all programs in the language have the desired properties. Variations of the system with different language features, notions of cost, and fine-grained control over productivity, could be considered depending on time and progress.
This is a 24 unit project for a student completing their Honours (COMP4550) or Advanced Masters (COMP8800). It will be co-supervised by Ranald Clouston (ANU) and Vineet Rajani (UNSW).
Requirements: Background and interest in mathematics and/or theoretical computer science. A strong result in COMP3610 / COMP6361 (Principles of Programming Languages) would be very helpful.