18
$\begingroup$

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?

$\endgroup$
  • 3
    $\begingroup$ I think that some research is being done at University of Bologna with the Matita proof assistant. See for example Formalizing Turing Machines. $\endgroup$ – Marzio De Biasi Nov 13 '17 at 17:22
  • $\begingroup$ Related: 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. $\endgroup$ – Joshua Grochow Nov 13 '17 at 18:17
  • $\begingroup$ 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. $\endgroup$ – Samuel Schlesinger Nov 14 '17 at 17:44
  • 1
    $\begingroup$ There's an answer to a similar question here, though it's more about proving specific complexity bounds than general complexity theory results $\endgroup$ – jmite Nov 14 '17 at 17:47
  • $\begingroup$ 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. $\endgroup$ – Samuel Schlesinger Nov 14 '17 at 17:50
6
$\begingroup$

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.)

$\endgroup$
  • 1
    $\begingroup$ Could you please give the complete reference so that the answer does not depend on the validity of the link? $\endgroup$ – holf Nov 22 '17 at 15:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.