Recent work in ramified recursion has led to a characterization of polynomial-time computability that admits certain forms of higher-type recursion. An extension of the Curry-Howard isomorphism to modal operators then leads to a new "feasible" arithmetic, I^1_2.

The provably convergent functions of I^1_2 are exactly the polynomial-time computable functions. But the definition contains no explicit reference to polynomials or to bounding terms. The system admits induction over formulas containing arbitrarily many alternation of unbounded quantifiers, albeit for "tier 0" values only. In I^1_2, ramification techniques are applied both to the domain objects and to the formulas of the logic.

The system is both intuitionistic and modal. Joint work with Alasdair Urquhart is currently in progress to develop a similar classical modal system, A^1_2.