MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

I am looking for references about efficient type theories, efficiency in the sense of computational complexity, and type theory in the sense of Martin-Lof's type theories. Has there been any studies with the goal of creating efficient versions of these theories?

Note: I am familiar with Stephen Cook and Alasdair Urquhart's theory $\mathsf{PV^\omega}$ and their "Functional Interpretations of Feasibly Constructive Arithmetic" paper from 1989 (doi:10.1145/73007.73017), but that is type theory in the sense of Kurt Godel's System $\mathsf{T}$. I am looking for feasible type theories in the sense of Martin-Lof's type theory.

share|cite|improve this question
I think feasibility and dependent product types don't fit together particularly well. Even for simple arrow types, there is a problem in getting an evaluation map $(f,x)\mapsto f(x):[X\to Y]\times X\to Y$ which is feasible (e.g. assuming polytime complexity). An elegant solution to that problem would be very interesting. – Wouter Stekelenburg Jun 29 '13 at 9:31

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.