Does the underlying computational calculus in type theories affect decidability?

Question

I'm looking for a high-level explanation although if that isn't possible or difficult, I'd prefer references to books/papers.

I understand that modern type theory is inspired by Curry-Howard correspondence. From the Wikipedia article on Curry-Howard correspondence:

The correspondence has been the starting point of a large spectrum of new research after its discovery, leading in particular to a new class of formal systems designed to act both as a proof system and as a typed functional programming language. ... This field of research is usually referred to as modern type theory.

Looking at the various type theories proposed and under development, I have a few basic questions:

1. Most modern type theories marry a type system with lambda calculus. Are there examples where a type theory uses a computational calculus other than lambda calculus?

2. At a very high level, if every modern type theory is a bundle of a type system and a computational calculus and the computational calculus is turing-complete (like lambda calculus), does the computational calculus in any way affect the decidability of decision problems like type checking, type inference, etc.? (AFAIK modern type theories tweak the type system while keeping the associated turing-complete computational calculus intact and just tweaking the type system affects decidability of type checking, type inference, etc.)

EDIT

NB: The distinction between Type Theory 1 and Type Theory 2 is based on their application in formal verification of programs and not based on the philosophy of type theory research. Also, the Program/Computation/Dynamic blocks are bigger as I guess existing programming languages have higher computational complexity than the type theories used for formal verification of their programs.

W.R.T. to the illustration above:

1) In type theory 1 methods, are type theories used both consistent and complete (w.r.t. Godel’s incompleteness theorem)? If there are type theories in proof assistants that are incomplete; leading to undecidable decision problems, how does the undecidability manifest in practical applications (like proving the correctness of a complex distributed systems protocol)?

2) In type theory 2 methods, what are the limitations of type theories in static analysis (w.r.t. Rice’s theorem)? Here, is decidability in type theories also affected by the computational model of programming language (eg. imperative vs functional languages)?

Answer 1

I don't think that the term "modern" helps distinguish anything. One way to explain is to draw a distinction between "behavioral", or "semantic", type theories and "formal", or "syntactic", type theories.

Behavioral type theories start with a notion of computation (say, an operational semantics of some kind), and define types as descriptions of program behavior, ie specifications. For example, one might specify that a function takes primes to primes as a description of how it behaves. Membership in a type is a matter of truth, not formal proof, and is never remotely axiomatizable, by Gödel's Theorem.

Formal, or syntactic, type theories are given by a collection of rules, including axioms as no-premise rules. They are inherently recursively enumerable, and never come close to any notion of truth. In particular such type theories, which often enjoy a (n empty) correspondence with a logical system (the poorly named C-H Correspondence), have no inherent meaning, computational or not. They are mere formalisms.

The two concepts may be linked by stipulating a priori that programs must be "well-typed" in the formal sense, with specifications of behavior refining types (for example, isolating the primes among the naturals). There are good reasons to take this viewpoint, namely that the rules prevent you from writing the code that you didn't want to write (eg, enforcing abstraction boundaries). But they also prevent you from writing the code that you do want to write (they define up-front what are the programs). The benefit of such restrictions is something called "the fundamental theorem", which states that syntactically well-formed programs enjoy behavioral properties associated to their types, a generalization of "type safety". In particular, the parametricity theorem is an example; it expresses that abstraction is properly enforced.

Answer 2

You are probably looking for computational type theory and you should probably look into realizability theory as well, which explains how to interpret type theory (and higher-order logic) on top of almost any kind of computational model.

Type theories based on a computational models that are Turing complete typically does not have decidable equality. An example of such a type theory is NuPRL.