Dependent type system with different computation model

Question

There exist various Turing-equivalent models of computation, such as lambda calculus, Turing machines, or register machines.

It seems that dependent type systems (like Coq, Agda, Idris, homotopy type theory) all have a lambda-calculus-based model of computation at their core. That's because they use term substitution ($\beta$-reduction) to relate the typing model to the computation model.

Can we swap out the lambda calculus at the core of dependent type systems for other computation models?

Or more generally, can we formulate a type system that lets us plug in our own computation model and its inference rules, subject to some set of consistency rules?