Dependent type system with different computation model
Yes, realizability theory allows you to model dependent type theory based on a variety of computational models, such as: Turing machines (with or without oracles), various $\lambda$-calculi, topological models of computation, sequential functionals, game-semantics computational models, and many others.

References:


Jaap van Oosten: Realizability: an introduction to its categorical side, Studies in Logic and the Foundations of Mathematics, vol. 152, Elsevier, 2008
You could also peek in Section 1.1. of my PhD thesis.