# Is there any work relating type systems and Cook-Reckhow proof systems?

An important subfield of computational complexity is proof complexity, mostly due to Cook and Reckhow. E.g. one notable result is that a proof system that has efficient proofs (i.e., in length polynomial to the formula being proven) for all tautologies could be constructed iff $coNP$ = $NP$. Other results deal with specific propositional calculus proof systems, showing that they all have superpolynomial proof lower-bounds. Is there any work relating type systems and type inference rules to the proof systems as defined in this theory?

In general, a cursory examination reveals that most discussions of type systems discuss computability (decidability/undecidability) with little discussion of finer complexity bounds (which may well exist in many finite models). Is there a reason why this is so (if indeed it is so)?

• Not an expert on proof complexity, but the type systems that type theorists discuss tend to be much more expressive than the classes that complexity theorists are interested in. E.g. the simply-typed λ-calculus with primitive recursion is probably the least expressive system type theory looks at, but every recursive function whose totality can be proved in first order logic (starting from the usual axioms for the elementary data types, eg Peano for natural numbers) can be expressed. The field of "implicit computational complexity" seeks to combine type theory with complexity theory. – Martin Berger May 8 '16 at 12:50

Cook-Reckhow propositional proof systems are nonunifrom. E.g. the computational complexity counterpart to the class of polynomial-size $\mathsf{Extended Frege}$ proofs is the nonuniform complexity class $\mathsf{P/poly}$. We have to look at their uniform counterparts: E.g. the proof complexity counterpart for $\mathsf{P}$ are bounded arithmetic theories like Cook's theory $\mathsf{PV}$ (standing for polynomial-time verifiable), Buss's theory $\mathsf{S}^1_2$, ...
Cook and Urquhart used Cook's theory $\mathsf{PV}$ to define a theory of higher-types polynomial-time computable functions $\mathsf{PV}^\omega$ in the following paper: