A compiler for cubical type theory

Cubical type theory is a new form of type theory that has received a lot of attention recently.

It can be seen as a kind of programming language that can be used both to write and verify programs and for statements and proofs in mathematics. This theory has some advantages over traditional (intensional) type theory. One example is that it provides good support for quotient types, which are similar to sets of equivalence classes.

It also has native support for the univalence axiom.A major goal of cubical type theory has been to ensure that "everything computes", i.e. that every term has a normal form. This ensures that cubical type theory can be used for programming.

However, so far there has been little emphasis on compiling languages based on cubical type theory, which means that their potential as highly expressive programming languages has not yet been borne out in practice.

Furthermore it is not obvious how to turn cubical programs into efficient machine code.The main goal of this project is to construct a compiler for a language based on cubical type theory.

The compiler should generate reasonably efficient code, and it should have support for erasure of data that is not relevant at run-time, like proofs showing that internal invariants of the code are not broken, so that such data does not slow down the generated programs.The plan is that the project should be carried out over four years by the PI, a PhD student, and a research engineer.