7
$\begingroup$

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.

Improve this question
$\endgroup$
1
  • 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, 2013 at 9:31

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.