The recent paper "A Type Theory for Synthetic $\infty$-Categories" proposes the syntax as the theory of the strict interval. In principle, any other suitable theory could be used instead. For instance, using Joyal’s theory of disks would yield a type theory in which to study $(\infty,n)$-categories ($\theta$ categories) in Rezk's style.
Any one know some work or references on a type theory to study higher categories, more specifically, $(\infty,n)$-categories and $(r,n)$-categories ?
I don't know of anyone who is specifically working on generalizing our paper to the $(\infty,n)$-case. But there have been other attempts to design a type theory for higher categories, such as Finster's opetopic type theory.
I take advantage of your post to point out to you that I built algebraic models of weak (\infty,m)-categories in different geometry :
Globular : http://www.tac.mta.ca/tac/volumes/30/22/30-22.pdf
Cubical : https://arxiv.org/pdf/1702.00336.pdf
Multiple : https://arxiv.org/pdf/1702.05206.pdf
For example these globular (\infty,0)-categories are models of globular \infty-groupoids. All these models are algebras for a specific monad. For example models of cubical (\infty,1)-categories are algebras for a specific monad on the category of cubical sets (see the arxiv above, because the cubical sets that I considered are a bit poorer than the usual one, those equipped with connections, etc.). Also it is highly probable that all these monads have arities, which means that behind it there are theories such that models of it correspond exactely to algebras for these monads.
Also it is not difficult to prove, for all integer m, that these globular models of (\infty,m)-categories are in fact weak infty-categories in Batanin's sense.
A big advantage of this approach is its simplicity : It follows an old idea of Batanin and Penon that "the weak must be coherently controlled by the strict", and you need to understand only the globular models to have a good picture of the rest, because the cubical models and the multiple models follow the same kind of construction.
Last thing which is very important : Behind all these monads there are adapted langages which permit to use basic technics of logic to built free (\infty,m)-categories, for all integer m, and for all geometry (globular, cubical, multiple). For example, if you fix an integer m, and a cubical set X, you can describe inductively the free cubical weak (\infty,m)-category F(X). This last point is not difficult to be guessed : Penon had already done it for the case of of the monad of globular infty-categories, in his article "Approche polygraphique des infini-catégories non-strictes, 1999", and my monads are similar to his monad ...
