<p>Maybe the keyword you are looking for is &quot;Implicit Complexity&quot;. It is more general than Curry-Howard correspondence, but several lines of research investigate along the axis you are interested in. You can check for instance the publications of <a href="http://perso.ens-lyon.fr/patrick.baillot/Publications/publications.html" rel="noreferrer">Patrick Baillot</a> for many references and pointers.</p>
<p>For a little self-promotion, here are for instance two recent papers [KPP1,KPP2] characterizing via the Curry-Howard correspondence on certain cyclic proofs the following complexity classes, depending on the logical rules incorporated or not in the cyclic proof system:</p>
<ul>
<li>Regular languages (no contraction, no cut) [KPP1]</li>
<li>DLogSpace (contraction, no cut) [KPP1]</li>
<li>Primitive recursive functions (cut, no contraction) [KPP2]</li>
<li>Gödel's System T (cut, contraction) [KPP2]</li>
</ul>
<p>[KPP1] <a href="https://hal.archives-ouvertes.fr/hal-02301651/document" rel="noreferrer">Cyclic Proofs and Jumping Automata</a>. Kuperberg, Pinault, Pous, FSTTCS 2019</p>
<p>[KPP2] <a href="https://hal.archives-ouvertes.fr/hal-02487175/document" rel="noreferrer">Cyclic Proofs, System T and the power of Contraction</a>. Kuperberg, Pinault, Pous, POPL 2021</p>

CC BY-SA 4.0
2021-04-17T13:42:24.473Z
thanks for elaborating on this
user1868607
CC BY-SA 4.0
2021-04-17T12:15:04.793Z
2021-04-17T21:07:09.397Z
2021-04-17T21:07:09.397Z
Denis
<p>I couldn't find documents elaborating on this: if the Curry Howard correspondence is to be interpreted as establishing a strong relation between proofs and programs, should there not be a strong relation between proof and computational complexity?</p>
<p>I'm asking this as a reference request.</p>

CC BY-SA 4.0
2021-04-17T09:50:51.907Z
Yes this is an active research field, here is a start: https://en.wikipedia.org/wiki/Proof_complexity
Denis
CC BY-SA 4.0
2021-04-17T11:22:28.960Z
@Denis Proof complexity is an active reasearch field indeed, but I am not aware of any proof complexity work related to the Curry–Howard correspondence. The proof systems studied in mainstream proof complexity are quite different from those to which the Curry–Howard correspondence applies. And, for that matter, the classes usually studied in computational complexity are also quite different from lambda calculi etc. that are subject to the Curry–Howard correspondence. Where there are connections between proof and computational complexity, they have completely different origins.
Emil Jeřábek
CC BY-SA 4.0
2021-04-17T11:25:56.660Z
@Denis So if you are actually aware of anything in proof complexity related to the Curry–Howard correspondence, please post it as a proper answer.
Emil Jeřábek
<cc.complexity-theory><reference-request><lo.logic><computability>
Proof and computational complexity
user1868607
# Proof and computational complexity

(Asked by: username_0 on 2021-04-16)

I couldn't find documents elaborating on this: if the Curry Howard correspondence is to be interpreted as establishing a strong relation between proofs and programs, should there not be a strong relation between proof and computational complexity?

I'm asking this as a reference request.

**Tags:** cc.complexity-theory, reference-request, lo.logic, computability
> **Comments:**
> **username_1**: Yes this is an active research field, here is a start: https://en.wikipedia.org/wiki/Proof_complexity  
> **username_2**: @Denis Proof complexity is an active reasearch field indeed, but I am not aware of any proof complexity work related to the Curry–Howard correspondence. The proof systems studied in mainstream proof complexity are quite different from those to which the Curry–Howard correspondence applies. And, for that matter, the classes usually studied in computational complexity are also quite different from lambda calculi etc. that are subject to the Curry–Howard correspondence. Where there are connections between proof and computational complexity, they have completely different origins.  
> **username_2**: @Denis So if you are actually aware of anything in proof complexity related to the Curry–Howard correspondence, please post it as a proper answer.  

---

## 1 answers

### Answer by username_1 on 2021-04-17. Score: 9 | Accepted answer

Maybe the keyword you are looking for is "Implicit Complexity". It is more general than Curry-Howard correspondence, but several lines of research investigate along the axis you are interested in. You can check for instance the publications of [Patrick Baillot](http://perso.ens-lyon.fr/patrick.baillot/Publications/publications.html) for many references and pointers.

For a little self-promotion, here are for instance two recent papers [KPP1,KPP2] characterizing via the Curry-Howard correspondence on certain cyclic proofs the following complexity classes, depending on the logical rules incorporated or not in the cyclic proof system:

* Regular languages (no contraction, no cut) [KPP1]
* DLogSpace (contraction, no cut) [KPP1]
* Primitive recursive functions (cut, no contraction) [KPP2]
* Gödel's System T (cut, contraction) [KPP2]

[KPP1] [Cyclic Proofs and Jumping Automata](https://hal.archives-ouvertes.fr/hal-02301651/document). Kuperberg, Pinault, Pous, FSTTCS 2019

[KPP2] [Cyclic Proofs, System T and the power of Contraction](https://hal.archives-ouvertes.fr/hal-02487175/document). Kuperberg, Pinault, Pous, POPL 2021

> **Comments:**
> **username_0**: thanks for elaborating on this  

---

