@article{NMO,
  author    = {Jasmin Christian Blanchette and Mathias Fleury and
    Dmitriy Traytel},
  title     = {Formalization of Nested Multisets, Hereditary Multisets,
    and Syntactic Ordinals},
  journal   = {Archive of Formal Proofs},
  month     = nov,
  year      = 2016,
  note      = {\url{http://isa-afp.org/entries/Nested_Multisets_Ordinals.html},
    Formal proof development},
  ISSN      = {2150-914x},
}

@article{C83,
  author    = "E. A. Cichon",
  title     = "A short proof of two recently discovered independence results
    using recursion theoretic methods",
  journal   = "Proceedings of the American Mathematical Society",
  volume    = 87,
  volume    = 4,
  pages     = "704--706",
  note      = "\doi{10.2307/2043364}",
  month     = apr,
  year      = 1983
}

@article{G44,
  author    = "R. L. Goodstein",
  title     = "On the restricted ordinal theorem",
  journal   = "Journal of Symbolic Logic",
  volume    = 9,
  issue     = 2,
  pages     = "33--41",
  note      = "\doi{10.2307/2268019}",
  year      = 1944
}

@incollection{T08,
  author    = "John Tromp",
  title     = "Binary Lambda Calculus and Combinatory Logic",
  booktitle = "Randomness And Complexity, from Leibniz To Chaitin",
  editor    = "Cristian S. Calude",
  publisher = "World Scientific Publishing Company",
  pages     = "237--260",
  month     = oct,
  year      = 2008
}

@misc{BLC,
  author    = "John Tromp",
  title     = "Binary lambda calculus",
  note      = "\url{https://tromp.github.io/cl/Binary_lambda_calculus.html}"
}
