@book{urban_isabelle_2019,
	title = {The {Isabelle} {Cookbook}: {A} {Gentle} {Tutorial} for {Programming} {Isabelle}/{ML}},
	author = {Urban, Christian},
	collaborator = {Berghofer, Stefan and Blanchette, Jasmin and Bohme, Sascha and Bulwahn, Lukas and Dawson, Jeremy and Kolanski, Rafal and Krauss, Alexander and Nipkow, Tobias and Schropp, Andreas and Sternagel, Christian},
	year = {2019},
}
@unpublished{wenzel_isabelle/isar_2019,
	title = {The {Isabelle}/{Isar} {Implementation}},
	author = {Wenzel, Makarius},
	collaborator = {Berghofer, Stefan and Haftmann, Florian and Paulson, Larry},
	year = {2019},
}
@unpublished{wenzel_isabelle/isar_2019-1,
	title = {The {Isabelle}/{Isar} {Reference} {Manual}},
	author = {Wenzel, Makarius},
	collaborator = {Ballarin, Clemens and Berghofer, Stefan and Blanchette, Jasmin and Bourke, Timothy and Bulwahn, Lukas and Chaieb, Amine and Dixon, Lucas and Haftmann, Florian and Huffman, Brian and Hupel, Lars and Klein, Gerwin and Krauss, Alexander and Kun{\v c}ar, Ond{\v r}ej and Lochbihler, Andreas and Nipkow, Tobias and Noschinski, Lars and Oheimb, David von and Paulson, Larry and Skalberg, Sebastian and Sternagel, Christian and Traytel, Dmitriy},
	year = {2019},
}
@article{paulson_natural_1986,
	title = {Natural {Deduction} as {Higher}-{Order} {Resolution}},
	volume = {3},
	number = {3},
	journal = {The Journal of Logic Programming},
	author = {Paulson, Lawrence C.},
	year = {1986},
	pages = {237--258},
}
@incollection{yang_comprehending_2017,
	address = {Heidelberg},
	title = {Comprehending {Isabelle}/{HOL}{\textquoteright}s {Consistency}},
	volume = {10201},
	isbn = {978-3-662-54433-4},
	booktitle = {Programming {Languages} and {Systems}},
	publisher = {Springer},
	author = {Kun{\v c}ar, Ond{\v r}ej and Popescu, Andrei},
	editor = {Yang, Hongseok},
	year = {2017},
	pages = {724--749},
}
@article{paulson_foundation_1989,
	title = {The {Foundation} of a {Generic} {Theorem} {Prover}},
	volume = {5},
	number = {3},
	journal = {Journal of Automated Reasoning},
	author = {Paulson, Lawrence C.},
	year = {1989},
	pages = {363--397},
}
@book{milner_definition_1997,
	address = {Cambridge, Massachusetts},
	title = {The {Definition} of {Standard} {ML} (revised)},
	isbn = {978-0-262-63181-5},
	publisher = {MIT Press},
	author = {Milner, Robin and Tofte, Mads and Harper, Robert and MacQueen, David},
	year = {1997},
	keywords = {ML (Computer program language)},
}
@book{nipkow_isabellehol_2002,
	address = {Heidelberg},
	title = {Isabelle/{HOL}: {A} {Proof} {Assistant} for {Higher}-{Order} {Logic}},
	isbn = {978-3-540-43376-7},
	publisher = {Springer Science \& Business Media},
	author = {Nipkow, Tobias and Paulson, Lawrence C. and Wenzel, Markus},
	year = {2002},
	keywords = {Computers / Information Technology, Computers / Intelligence (AI) \& Semantics, Mathematics / Logic, Mathematics / Discrete Mathematics, Computers / Computer Science, Computers / Programming / General, Philosophy / Logic, Computers / Programming Languages / General},
}
