Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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|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
add comment

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.