@book{ccama,
  author = {Sanjeev Arora and Boaz Barak},
  isbn = {978-0-521-42426-4},
  publisher = {Cambridge University Press},
  title = {Computational Complexity: A Modern Approach},
  url = {https://theory.cs.princeton.edu/complexity/book.pdf},
  year = 2006
}

@article{Cook,
    author={Stephen A. Cook},
    title={The complexity of theorem-proving procedures},
    journal={Proceedings of the third annual ACM symposium on Theory of computing},
    year={1971}
}

@article{Levin,
    author = {Levin, L. A.},
    journal = {Problems of Information Transmission},
    number = 3,
    pages = {265--266},
    title = {Universal sequential search problems},
    volume = 9,
    year = 1973
}

@inproceedings{Gher2021MechanisingCT,
    title={Mechanising Complexity Theory: The {C}ook-{L}evin Theorem in {C}oq},
    author={Lennard G{\"a}her and Fabian Kunze},
    booktitle={ITP},
    year={2021}
}

@inproceedings{Forster2017WeakCL,
    title={Weak Call-by-Value Lambda Calculus as a Model of Computation in {C}oq},
    author={Yannick Forster and Gert Smolka},
    booktitle={ITP},
    year={2017}
}

@inproceedings{Gamboa2004AMP,
    title={A Mechanical Proof of the {C}ook-{L}evin Theorem},
    author={Ruben Gamboa and John R. Cowles},
    booktitle={TPHOLs},
    year={2004}
}

@article{Universal_Turing_Machine-AFP,
  author  = {Jian Xu and Xingyuan Zhang and Christian Urban and Sebastiaan J. C. Joosten},
  title   = {Universal Turing Machine},
  journal = {Archive of Formal Proofs},
  month   = feb,
  year    = 2019,
  note    = {\url{http://isa-afp.org/entries/Universal_Turing_Machine.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@article{Multiset_Ordering_NPC-AFP,
    author  = {René Thiemann and Lukas Schmidinger},
    title   = {The Generalized Multiset Ordering is {NP}-Complete},
    journal = {Archive of Formal Proofs},
    month   = apr,
    year    = 2022,
    note    = {\url{https://isa-afp.org/entries/Multiset_Ordering_NPC.html},
                Formal proof development},
    ISSN    = {2150-914x},
}

@book{lv-aikc,
  author = {Li, Ming and Vitányi, Paul M. B.},
  title = {An Introduction to Kolmogorov Complexity and Its Applications},
  edition = {4th},
  publisher = {Springer},
  series = {Texts in Computer Science},
  year = 2019,
  isbn = {978-3-030-11297-4}
}

@misc{cz-dtime,
    author = "Scott Aaronson",
    title = "Complexity Zoo",
    url = "https://complexityzoo.net/Complexity_Zoo",
    note = {\url{https://complexityzoo.net/Complexity_Zoo}}
}

@article{Multitape_To_Singletape_TM-AFP,
  author  = {Christian Dalvit and René Thiemann},
  title   = {A Verified Translation of Multitape Turing Machines into Singletape Turing Machines},
  journal = {Archive of Formal Proofs},
  month   = {November},
  year    = {2022},
  note    = {\url{https://isa-afp.org/entries/Multitape_To_Singletape_TM.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@book{sipser2006,
  author={Michael Sipser},
  title={Introduction to the Theory of Computation},
  edition={2nd},
  isbn={9780619217648},
  year={2006},
  publisher={Thomson Course Technology}
}

@misc{acl2,
  author       = {Robert S. Boyer and J Strother Moore and Matt Kaufmann},
  title        = {{ACL2}},
  note         = {\url{https://www.cs.utexas.edu/users/moore/acl2/}}
}

@misc{coq,
  author       = {The Coq Development Team},
  title        = {The {C}oq Proof Assistant},
  month        = jan,
  year         = 2022,
  publisher    = {Zenodo},
  version      = {8.15},
  doi          = {10.5281/zenodo.5846982},
  url          = {https://doi.org/10.5281/zenodo.5846982}
}

@article{hs65,
  title={On the Computational Complexity of Algorithms},
  author={Juris Hartmanis and Richard Edwin Stearns},
  journal={Transactions of the American Mathematical Society},
  year={1965},
  volume={117},
  pages={285-306}
}