An arithmetic for polynomial-time computation

We define a restriction LHA of Heyting arithmetic HA with the property that all extracted programs are feasible. The restrictions consist in linearity and ramification requirements.