@string{JAR="J. Automated Reasoning"}
@string{JFP="J. Functional Programming"}
@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
@string{Springer="Springer"}

@inproceedings{BerghoferN-TPHOLs00,author={Stefan Berghofer and Tobias Nipkow},
title={Proof terms for simply typed higher order logic},
booktitle={Theorem Proving in Higher Order Logics},
editor={J. Harrison and M. Aagaard},
year=2000,publisher=Springer,series=LNCS,volume=1869,pages="38--52"}


@article{Paulson-JAR-89,author="Lawrence C. Paulson",
title="The Foundation of a Generic Theorem Prover",
journal=JAR,year=1989,volume=5,pages="363--397"}


@inproceedings{tphol/Wenzel97,
  author    = {Markus Wenzel},
  editor    = {Elsa L. Gunter and
               Amy P. Felty},
  title     = {Type Classes and Overloading in Higher-Order Logic},
  booktitle = {Theorem Proving in Higher Order Logics, {TPHOLs}'97},
  series    = LNCS,
  volume    = {1275},
  pages     = {307--322},
  publisher = Springer,
  year      = {1997},
  url       = {https://doi.org/10.1007/BFb0028402},
}

@misc{implementation, author={Makarius Wenzel}, title={The Isabelle/Isar Implementation},note={https://isabelle.in.tum.de/doc/implementation.pdf}}

@inproceedings{cade28,
  author = {Tobias Nipkow and Simon Roßkopf},
  title = {Isabelle's Metalogic: Formalization and Proof Checker},
  editor = {A. Platzer, G. Sutcliffe},
  series = LNCS,
  booktitle = {28th International Conference on Automated Deduction (CADE-28)},
  publisher = Springer,
  year = {2021}
}
