<p>In the following paper my colleague Uli Schöpp presents a formal verification (in Coq)  of a nontrivial result by Cook and Rackoff on the computational power of graph automata. <a href="https://scholar.google.at/scholar?oi=bibs&amp;cluster=4944920843669159892&amp;btnI=1&amp;hl=de" rel="noreferrer">https://scholar.google.at/scholar?oi=bibs&amp;cluster=4944920843669159892&amp;btnI=1&amp;hl=de</a> (Schöpp, U. (2008). A formalised lower bound on undirected graph reachability. In Logic for Programming, Artificial Intelligence, and Reasoning (pp. 621-635). Springer Berlin/Heidelberg.)</p>

CC BY-SA 3.0
2017-11-22T15:29:12.513Z
Could you please give the complete reference so that the answer does not depend on the validity of the link?
holf
CC BY-SA 3.0
2017-11-22T15:23:56.667Z
2017-11-22T15:38:00.097Z
2017-11-22T15:38:00.097Z
Martin Hofmann
<p>A nice example is <strong>Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, David Nowak:
<em>Formal proof of polynomial-time complexity with quasi-interpretations.</em> CPP 2018: 146-157</strong></p>

<p>Their abstract (my emphasis):</p>

<blockquote>
  <p><strong>We present a Coq library that allows for readily proving that a function is computable in polynomial time.</strong> It is based on quasi-interpretations that, in combination with termination ordering, provide a characterisation of the class FP of functions computable in polynomial time. At the heart oft his formalisation is a proof of soundness and extensional completeness. Compared to the original paper proof, we had to fill a lot of not so trivial details that were left to the reader and fix a few glitches. To demonstrate the usability of our library, we apply it to the modular exponentiation.</p>
</blockquote>

CC BY-SA 4.0
2021-04-28T12:53:35.727Z
This work is also related to [A Formalization of Polytime Functions](https://link.springer.com/chapter/10.1007/978-3-642-22863-6_11).
Clément
CC BY-SA 4.0
2020-04-18T17:57:21.760Z
2020-04-18T17:57:21.760Z
Clément
<p>Is there any ongoing project to formally verify the theorems and proofs of complexity theory using a proof assistant like Coq? Are there any boundaries to doing this?</p>

CC BY-SA 3.0
2017-11-13T17:22:58.943Z
I think that some  research is being done at University of Bologna with the Matita proof assistant. See for example [Formalizing Turing Machines](http://www.cs.unibo.it/~asperti/PAPERS/turing.pdf).
Marzio De Biasi
CC BY-SA 3.0
2017-11-13T18:17:16.027Z
Related: https://cstheory.stackexchange.com/q/4052/129.
 Some of the answers even talk about Coq, and others mention results that could be interpreted as theoretical barriers to this project, though likely they are not barriers in practice.
Joshua Grochow
CC BY-SA 3.0
2017-11-14T17:44:56.837Z
Thanks, that question was great @JoshuaGrochow, so glad I learned about that Hartmannis monograph. If I understand, the barrier would then be making sure that the complexity classes you define are what you think they are rather than the "provable in Coq" version.
Samuel Schlesinger
CC BY-SA 3.0
2017-11-14T17:47:53.677Z
There's an answer to a similar question [here](https://cs.stackexchange.com/questions/83700/theorem-prover-for-complexity-theoretic-reductions/83703#83703), though it's more about proving specific complexity bounds than general complexity theory results
Joey Eremondi
CC BY-SA 3.0
2017-11-14T17:50:07.547Z
Right that's relevant though. I'm curious about ways in which the underlying type system could help, like by including some notions of complexity in the types of functions. Of course this would lead to a wide range of equalities but I think that's what we have in complexity naturally anyways.
Samuel Schlesinger
CC BY-SA 3.0
2017-11-14T20:45:13.773Z
In addition to jmite's answer on the question linked to, I think there's some way to formalize complexity bounds using so-called "implicit complexity theory," which might be more easily formalized in something like Coq (or whatever the current favorite is for computer implementations of univalent foundations). My starting reference for this line of work is dal Lago's papers, but @NeelKrishnaswami might have more to say on this. Been wanting to learn this stuff for a while...
Joshua Grochow
CC BY-SA 3.0
2017-11-14T20:52:19.540Z
Right, with a brief look over the description of implicit complexity theory on Wikipedia it appears that this would be a cheap way for me to avoid a lot of minutia but I must read more and see if it is complete for what I want to do.
Samuel Schlesinger
<cc.complexity-theory><complexity><proof-assistants>
Formally Verified Complexity Theory
Samuel Schlesinger
# Formally Verified Complexity Theory

(Asked by: username_0 on 2017-11-13)

Is there any ongoing project to formally verify the theorems and proofs of complexity theory using a proof assistant like Coq? Are there any boundaries to doing this?

**Tags:** cc.complexity-theory, complexity, proof-assistants
> **Comments:**
> **username_1**: I think that some  research is being done at University of Bologna with the Matita proof assistant. See for example [Formalizing Turing Machines](http://www.cs.unibo.it/~asperti/PAPERS/turing.pdf).  
> **username_2**: Related: https://cstheory.stackexchange.com/q/4052/129.  Some of the answers even talk about Coq, and others mention results that could be interpreted as theoretical barriers to this project, though likely they are not barriers in practice.  
> **username_0**: Thanks, that question was great @JoshuaGrochow, so glad I learned about that Hartmannis monograph. If I understand, the barrier would then be making sure that the complexity classes you define are what you think they are rather than the "provable in Coq" version.  
> **username_3**: There's an answer to a similar question [here](https://cs.stackexchange.com/questions/83700/theorem-prover-for-complexity-theoretic-reductions/83703#83703), though it's more about proving specific complexity bounds than general complexity theory results  
> **username_0**: Right that's relevant though. I'm curious about ways in which the underlying type system could help, like by including some notions of complexity in the types of functions. Of course this would lead to a wide range of equalities but I think that's what we have in complexity naturally anyways.  
> **username_2**: In addition to jmite's answer on the question linked to, I think there's some way to formalize complexity bounds using so-called "implicit complexity theory," which might be more easily formalized in something like Coq (or whatever the current favorite is for computer implementations of univalent foundations). My starting reference for this line of work is dal Lago's papers, but @NeelKrishnaswami might have more to say on this. Been wanting to learn this stuff for a while...  
> **username_0**: Right, with a brief look over the description of implicit complexity theory on Wikipedia it appears that this would be a cheap way for me to avoid a lot of minutia but I must read more and see if it is complete for what I want to do.  

---

## 2 answers

### Answer by username_4 on 2017-11-22. Score: 10

In the following paper my colleague Uli Schöpp presents a formal verification (in Coq) of a nontrivial result by Cook and Rackoff on the computational power of graph automata. <https://scholar.google.at/scholar?oi=bibs&cluster=4944920843669159892&btnI=1&hl=de> (Schöpp, U. (2008). A formalised lower bound on undirected graph reachability. In Logic for Programming, Artificial Intelligence, and Reasoning (pp. 621-635). Springer Berlin/Heidelberg.)

> **Comments:**
> **username_5**: Could you please give the complete reference so that the answer does not depend on the validity of the link?  

---

### Answer by username_6 on 2020-04-18. Score: 6

A nice example is **Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, David Nowak:
*Formal proof of polynomial-time complexity with quasi-interpretations.* CPP 2018: 146-157**

Their abstract (my emphasis):

> **We present a Coq library that allows for readily proving that a function is computable in polynomial time.** It is based on quasi-interpretations that, in combination with termination ordering, provide a characterisation of the class FP of functions computable in polynomial time. At the heart oft his formalisation is a proof of soundness and extensional completeness. Compared to the original paper proof, we had to fill a lot of not so trivial details that were left to the reader and fix a few glitches. To demonstrate the usability of our library, we apply it to the modular exponentiation.

> **Comments:**
> **username_6**: This work is also related to [A Formalization of Polytime Functions](https://link.springer.com/chapter/10.1007/978-3-642-22863-6_11).  

---

