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.)
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)?