TL; DR: There are. But there are also severe difficulties that only have unsatisfactory solutions.
Let's see what bad things will happen, so we can attempt to fix it. The first thing when trying to turn sequent calculus into a type theory, is that there are many equivalent but meaninglessly different terms. Consider the left $\wedge$-introduction rule:
$$\frac{A, B, \Delta \vdash \Gamma}{A \wedge B, \Delta \vdash \Gamma}$$
This is very well and all, and we might try to assign the syntax like
$$\frac{t : (x{:}A, y{:}B, \Delta \vdash \Gamma)}{t[p \sim x, y] : (p{:}A \wedge B, \Delta \vdash \Gamma)}$$
it would bind the variables $x,y$ in $t$, as well as creating a free variable $p$. But consider a derivation from $A_1, \dots, A_{10} \vdash B$ to $A_1 \wedge A_2, A_3 \wedge A_4,\dots, A_9 \wedge A_{10} \vdash B$. Since we have five $\wedge$-introduction, we have $5! = 120$ different terms. Which should be normal? There's no canonical way to decide. And therefore such a syntax faces severe metatheoretical problems, because our intended semantics doesn't contain the order information while the syntax does. So even if you construct a model to prove stuff, the model will be very exotic and won't resemble anything familiar or expected.
The fundamental reason that this happens is that the sequent calculus is unfocused. The rules can operate on any formula in random, and as long as they don't affect each other, the order of these rules shouldn't matter.
One way to deal with this is the proof net approach by Girard. But just checking the validity of proof nets seems to be very hard, and there are various criteria and algorithms. They won't look like a type theory anyway. So we won't go down that rabbit hole for now.
Another way to deal with this is, well, obviously, by introducing focus.
In intuitionistic logic, there are only one formula on the right of $\vdash$, and the focus is naturally on that formula. This makes all the inference rules sequential, and we can pack it up into a nice term syntax.
In classical sequent calculus, we have to manually mark a formula as "focused", and have all the rules operate on it. We also have rules to lose and gain focus.
Let's use square brackets to mark the focus (it's not the standard notation, but I think it's clearer). So for right $\to$-introduction, we have a focused formula on the right:
$$\frac{t : (\Gamma, x{:}A \vdash [B], \Delta)}{\lambda x.t : (\Gamma \vdash [A \to B], \Delta) }$$
Looks nice. And for left $\to$-introduction (remember that there are no elimination rules in sequent calculus, we only have right/left introduction, and the cut rule), we have to focus on the left:
$$\frac{t : (\Gamma \vdash [A], \Delta) \quad c : (\Gamma, [B] \vdash \Delta)}{t\cdot c : (\Gamma, [A \to B] \vdash \Delta)}$$
(If you feel unfamiliar with this, grab a book an sequent calculus and refresh yourself. This is exactly the left-introduction rule for $\to$.)
And, as we said, we need the cut rule for anything interesting to happen:
$$\frac{t : (\Gamma \vdash [A], \Delta) \quad c : (\Gamma, [A] \vdash \Delta)}{\langle c | t \rangle : (\Gamma \vdash \Delta)}$$
We also need ways to unfocus (the cut rule gives the way to focus). Since unfocused formulas corresponds to variables (think intuitionistic logic, where all the formulas on the left are unfocused, and they are each assigned a variable; the focused formula on the right doesn't have a variable), we need to kill a variable. What kills a variable? A binder. So here enters our $\mu$ binder:
$$\frac{E : (\Gamma \vdash \alpha{:}A, \Delta)}{\mu \alpha. E : (\Gamma \vdash [A], \Delta)}$$
Dually we have the $\tilde\mu$ binder:
$$\frac{E : (\Gamma, x {:} A \vdash \Delta)}{\tilde\mu a. E : (\Gamma, [A] \vdash \Delta)}$$
And last but not lease, we of course need to enable terms to refer to variables, or else there's no good doing anything!
$$\frac{}{\alpha : (\Gamma, [A] \vdash \alpha{:}A, \Delta)} \quad \frac{}{x : (\Gamma, x{:} A \vdash [A], \Delta)}$$
Now we have seen three types of things:
- Terms $t$ have their focus on the right. They are very much like the terms in our usual intuitionistic type theory, as you can see that every rule with the focus on the right looks familiar.
- Coterms $c$ have their focus on the left. They are like holes, or continuations. But it's fine if you don't get any intuition for them.
- Commands $E$ (or as Zeilberger calls it, programs) don't have a focus. They are what you get when you put together a term of type $A$ and a continuation demanding a term of type $A$.
Well, that's nice, but as you have mentioned, we now have normalization problems. Also, although you said there is a $\lambda\mu$-cube, the cube is defined in Curry style. And as is well known, even $\lambda 2$ in Curry style has undecidable type checking, making life harder for proof assistants. Apart from decidability, $\lambda \mu$-calculus is actually equationally inconsistent. This means that $\lambda xy. x = \lambda xy.y$. This is fine in simple types, and doesn't affect logical consistency which says the empty type has no closed terms. But in dependent types, equational inconsistency means that any two types will be equal, which further entails logical inconsistency.
The ultimate reason for this is because we haven't chosen a canonical evaluation order. Actually, if you settle on call-by-name, or call-by-value, or any evaluation strategy, as long as you don't change your mind halfways, you do get good normalization properties. However, this arbitrarily chosen order also has a negative impact in dependent types, since some perfectly legit types would have no terms, because they don't reduce in the specific evaluation order to the desired form.
To solve the ad-hoc-ness of the chosen evaluation order, we can add polarity to the types. I linked to a paper in the comments. There's also Zeilberger's thesis. And in my opinion this settles the ad-hoc problem in a
pretty elegant way.
But you still have problems when switching to dependent types, because now types may carry computations. And there are partial solutions which only allows types to be dependent on positive values. The link also explains the difficulties in more depth.
And finally, I should really mention Shulman's paper encoding a logic that is symmetric (although not perfectly classical, of course; the negation is involutive, though) purely inside intuitionistic type theory.
