3
$\begingroup$

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?

$\endgroup$
6
$\begingroup$

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.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.