License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2021.20
URN: urn:nbn:de:0030-drops-139154
Go to the corresponding LIPIcs Volume Portal

Gäher, Lennard ; Kunze, Fabian

Mechanising Complexity Theory: The Cook-Levin Theorem in Coq

LIPIcs-ITP-2021-20.pdf (0.8 MB)


We mechanise the Cook-Levin theorem, i.e. the NP-completeness of SAT, in the proof assistant Coq. We use the call-by-value λ-calculus L as the model of computation to formalise time complexity, the class NP, and polynomial-time reductions. The latter two notions agree with the usual characterisations via Turing machines (TMs), as L and TMs are polynomial-time equivalent.
The use of L as the computational model, as opposed to TMs, significantly eases program verification and the derivation of resource bounds. However, for showing the NP-hardness of SAT, computations of L need to be encoded in SAT, which is complicated by L’s more complex computational structure. Thus, the polynomial-time reduction chain to SAT employs TMs as an intermediate problem, for which we neatly factor out a known textbook reduction from TMs to SAT. Still, all reduction functions are implemented and analysed in L.
To the best of our knowledge, this is the first result in computational complexity theory that has been mechanised with respect to any concrete computational model.
We discuss what makes this area of computer science hard to mechanise and highlight the design choices which enable our mechanisations.

BibTeX - Entry

  author =	{G\"{a}her, Lennard and Kunze, Fabian},
  title =	{{Mechanising Complexity Theory: The Cook-Levin Theorem in Coq}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-139154},
  doi =		{10.4230/LIPIcs.ITP.2021.20},
  annote =	{Keywords: computational model, NP completeness, Coq, Cook, Levin}

Keywords: computational model, NP completeness, Coq, Cook, Levin
Collection: 12th International Conference on Interactive Theorem Proving (ITP 2021)
Issue Date: 2021
Date of publication: 21.06.2021
Supplementary Material: Software (Code Repository): archived at:

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI