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.

  • 1
    $\begingroup$ 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. $\endgroup$ – Wouter Stekelenburg Jun 29 '13 at 9:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.