System $F$ is quite expressive. As proved by Girard here, the functions of type $\mathbb{N}\rightarrow\mathbb{N}$ (where $\mathbb{N}$ is defined to be $\forall X.\ X\rightarrow (X\rightarrow X)\... View answer Accepted answer 40 votes I strongly disagree with the "find a list of open problems" approach. Usually open problems are quite hard to make progress on, and I'm thoroughly unconvinced that good research is done by tackling ... View answer 27 votes There have been recent developments in dependent type theory which relate type systems to homotopy types. This is now a relatively small field, but there is a lot of exciting work being done right ... View answer 25 votes I've already answered somewhat, but I'll try to give a more detailed overview of the type theoretical horizon, if you will. I'm a bit fuzzy on the historical specifics, so more informed readers will ... View answer Accepted answer 23 votes In general you cannot determine complexity, even for halting programs: let$T$be some arbitrary Turing machine and let$p_T$be the program (that always returns 0): input: n run T for n steps if T ... View answer 22 votes I've often wanted to try and summarize each dimension of the$\lambda$-cube and what they represent, so I'll give this one a shot. But first, one should probably try to dis-entangle various issues. ... View answer 22 votes$\mathrm{Prop}$is impredicative, which create a very expressive proof system. However it is "too" expressive in the following sense: $$\mathrm{impredicative\ Prop} + \mathrm{large\ elimination} + \... View answer 21 votes Alright I'll give a crack at it: In general for a given type system T, the following is true: If all well-type terms in the calculus T are normalizing, then T is consistent when viewed as a ... View answer Accepted answer 20 votes The short answer is yes, MLTT can reasonably be equated with CIC without impredicative Prop. The main technical issue is that there are dozens of variants when one talks about Martin-Löf Type Theory ... View answer Accepted answer 20 votes The short answer to your question 1 is no, but for perhaps subtle reasons. First of all, System F and F_\omega cannot express the first-order theory of arithmetic, and even less the consistency ... View answer Accepted answer 17 votes The answer is it depends what you mean by Term Rewrite System. When it was introduced, the concept of Term Rewrite Systems, or TRSes, described what is now called first order TRSes, which is simply a ... View answer 16 votes A quick bit of googling gives this for the RSA paper: Rivest stayed up all night, preparing the manuscript describing the code before he handed it to Adleman. He had listed the paper's authors in ... View answer 15 votes You might want to check out Liquid Haskell, which allow working with type refinements rather than dependent types. Type refinements can be seen as a restricted logical language that allow you to ... View answer Accepted answer 14 votes In general, what we usually call the logical relations argument isn't really linked to impredicativity: the main idea is simply to interpret terms in some abstract algebra \cal A, and to represent ... View answer 14 votes The author is not misinformed, I'm afraid; it's part of the development process of any computer scientist to go through several phases: Phase 1: \alpha-equivalence is easy! Why is everyone making a ... View answer Accepted answer 13 votes Because one of the principal applications of Type Theory in formalizations has been to study programing languages and computation in general, a lot of thought has gone into ways of representing ... View answer Accepted answer 13 votes I'm going to elaborate my comments into an answer. The origins of predicative type theory are almost as old as type theory itself, since one of Russel's motivations was to ban "circular" definitions ... View answer Accepted answer 13 votes This is an interesting question! As Anthony's answer suggests, one can use the usual approaches to compiling a non-dependent functional language, provided you already have an interpreter to evaluate ... View answer 13 votes I'm not sure I have a satisfactory answer to your question, but if you consider Pure Type Systems, which are a generalization of the systems found in the lambda cube (a thorough, if somewhat dated ... View answer Accepted answer 12 votes The presentation of functional elimination using \mathrm{funsplit} is most definitely not a usual occurrence in most treatments of type theory. However, I believe that this form is indeed the "... View answer Accepted answer 11 votes To my knowledge, no machine checked proof of a complex mathematical development has ever been retracted. As Andrej points out though, it occasionally happens that soundness-breaking bugs do crop up ... View answer Accepted answer 11 votes You are correct, there is an error in that paper, and the rule should indeed read:$$\frac{\Gamma\vdash M:\Delta}{\Gamma\vdash M\cong M} $$the use of jugements of this style for equality (sometimes ... View answer 11 votes There are absolutely some relationships between the semantics and practice of OOP and category theory. This is somewhat unsurprising since both fields attempt to give a principled generic account of ... View answer 11 votes Applying higher homotopy-theoretic ideas to CS is still a very nascent field! My understanding is that it's not even that old as a mathematical field. Certainly HoTT is the central impetus for such ... View answer Accepted answer 11 votes The distinction is this: if STLC is taken as a primitive language at the type-level adding constructors and a small number of axioms is sufficient to give you the full expressive power of HOL. Taking ... View answer 11 votes Barendregts Lambda Calculi with Types is more advanced, but it covers some important topics in the "classical" theory of types. View answer 11 votes Another possible answer to Neel's perfectly correct one: Suppose that there is a combinator E, well-typed in system F such that the above condition holds. The type of E is:$$ E : \forall \alpha.\... View answer Accepted answer 10 votes I'm going to assume that by$\mathrm{Fix}$you mean a new type constructor $$\frac{\Gamma\vdash F:*\rightarrow *}{\Gamma\vdash \mathrm{Fix}\ F:*}$$ Along with the conversion rule$\mathrm{Fix}\ F\...

Certainly the decision problem Given a (pre-)term $a$ Is there a type $A$ such that $\vdash a :A$ is derivable in MLTT? Sometimes written $\vdash a\ :\ ?$ (and called the type inference problem) ...
It might be useful to quickly give the counter-example to CR in typed calculi with $\beta$ and $\eta$: $$t=\lambda x:A.(\lambda y:B.\ y)\ x$$ And we have $$t\rightarrow_\beta \lambda x: A.x$$ and \$...