The main themes of the project, articulated as work packages, are:
- Proof Theory, Type Theory, and Constructive Set Theory: Studying systems which are simultaneously able to compute and prove the correctness of computations means we need to study the interrelated areas of type theory, proof theory and constructive set theory. Type theory is an abstraction of a programming language where non-fundamental details are removed, proof theory is a technique which tells us what type theories can and can’t do, and constructive set theory allows us to ensure that when we prove something, no non-implementable aspects are used in the proof.
- Constructive Topology and Analysis: Of particular sophistication is computation between real numbers and, more generally, infinitary structures. This necessitates the development of constructive versions of the standard branches of mathematics that deal with real numbers and the like, that is the development of constructive analysis and constructive topology.
- Homotopy Type Theory: One of the major problems within correct by construction programming is equality. We won’t have a proper understanding of the logic of computation until we can understand the logic of computing proofs that various computational entities are equal. The nature of equality was always been a major philosophical issue, but now, the need for a constructive and computational treatment of equality has become a fundamental problem inhibiting progress in a number of areas. This theme focusses on a major new insight into the problem, namely homotopy type theory.
- Categorical Logic: Logic has always been greatly influenced by its model theory which has a more algebraic flavour and this is no different for the sorts of logics needed by correct by construction programming. Of particular relevance is category theory which has been shown to be a powerful tool for understanding logical theories. Within this work package we will deepen our understanding of the logics needed for correct by construction programming by developing their categorical semantics.
- Programming Languages for Correct by Construction Programming: Of course, once we have clean logical abstractions capable of supporting correct by construction programming, we need to actually turn them into the programming languages, idioms, and abstractions of the future. In this section we will focus on a number of concrete ways to do this.
- Correct by Construction Programs over Continuous Data: Similarly, we require dedicated programming languages, idioms and abstractions tailored to correct by construction programs which manipulate continuous data, a conceptually different framework which needs its own, distinct treatment.
- Correct by Construction Programs with Limited Resources: And finally, as computation becomes ever more localised and autonomous, we need to understand how all of the above can be executed in a low resourced environment.