At the core of the modern understanding of the Curry-Howard correspondence between proofs and programs is the connection between, on the one hand, the syntax of logic and type theory, and on the other, certain mathematical structures, often taking the form of structured categories and related objects. In one of its most well-known incarnations, for example, we can see the simply typed lambda calculus as a syntactic notation for morphisms in a cartesian closed category. Equivalently, free cartesian closed categories can be constructed directly from syntax in a way which gives them a well-understood computational interpretation.

With the recent advances in understanding the homotopical nature of dependent type theory, as well as the parallel development of tractable models of higher categories, it is natural to wonder if this classical correspondence between syntax, semantics and computation can be extended in a direct way to higher structures. That is, can we find some kind of natural syntactic description of higher structured categories? In this talk I will explain one possibility for such a description of monoidal closed higher categories using a graphical syntax based on opetopes.