Abstract

Recent work by Bezem, Coquand, and Huber has reformulated the mathematical underpinnings of HoTT using cubical sets, which is a step towards allowing a more computational interpretation of HoTT. In this talk I will discuss how this reformulation of HoTT using cubical sets allows the possibility of exploration into how we can use this new cubical foundation to provide a way to talk about what I am calling Directed Homotopy Type Theory, using directed cubical sets. I will explain some background related to this work and show how we could use this new theory to encode concurrency at the type level of the program using the ideas developed by Fajstrup, Raussen, and Goubalt in their theory on (directed) algebraic topology and concurrency.

This is a forward-looking talk that seeks to motivate research into Directed Homotopy Type Theory and seeks to show how it could be useful to other areas of computer science, and programming languages in general.