@incollection{blanchette_types_2016,
	address = {Heidelberg},
	title = {From {Types} to {Sets} by {Local} {Type} {Definitions} in {Higher}-{Order} {Logic}},
	volume = {9807},
	isbn = {978-3-319-43144-4},
	booktitle = {Interactive {Theorem} {Proving}},
	publisher = {Springer},
	author = {Kun{\v c}ar, Ond{\v r}ej and Popescu, Andrei},
	editor = {Blanchette, Jasmin Christian and Merz, Stephan},
	year = {2016},
	pages = {200--218},
}
@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},
}
@incollection{immler_smooth_2019,
	address = {New York},
	series = {{CPP} 2019},
	title = {Smooth {Manifolds} and {Types} to {Sets} for {Linear} {Algebra} in {Isabelle}/{HOL}},
	isbn = {978-1-4503-6222-1},
	booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} {International} {Conference} on {Certified} {Programs} and {Proofs}, {CPP} 2019, {Cascais}, {Portugal}},
	publisher = {ACM},
	author = {Immler, Fabian and Zhan, Bohua},
	editor = {Mahboubi, Assia and Myreen, Magnus O.},
	year = {2019},
	keywords = {Formalization of Mathematics, Higher Order Logic, Isabelle, Manifolds},
	pages = {65--77},
}
@misc{immler_automation_2019,
	title = {Automation for unverloading definitions},
	url = {http://isabelle.in.tum.de/repos/isabelle/rev/ab5a8a2519b0},
	journal = {isabelle/changeset},
	author = {Immler, Fabian},
	year = {2019},
}
@phdthesis{kuncar_types_2015,
	address = {Munich},
	title = {Types, {Abstraction} and {Parametric} {Polymorphism} in {Higher}-{Order} {Logic}},
	school = {Technische Universit{\"a}t M{\"u}nchen},
	author = {Kun{\v c}ar, Ond{\v r}ej},
	year = {2015},
}
@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},
}
@phdthesis{wenzel_isabelle/isar_2001,
	address = {Munich},
	title = {Isabelle/{Isar} {\textemdash} {A} {Versatile} {Environment} for {Human}-{Readable} {Formal} {Proof} {Documents}},
	school = {Technische Universit{\"a}t M{\"u}nchen},
	author = {Wenzel, Markus M.},
	year = {2001},
}
@inproceedings{gilcher_conditional_2017,
	address = {Bras{\'i}lia, Brazil},
	title = {Conditional {Parametricity} in {Isabelle}/{HOL}},
	booktitle = {{TABLEAUX}/{FroCoS}/{ITP}},
	author = {Gilcher, Jan and Lochbihler, Andreas and Traytel, Dmitriy},
	year = {2017},
}
@article{divason_perron-frobenius_2016,
	title = {Perron-{Frobenius} {Theorem} for {Spectral} {Radius} {Analysis}},
	journal = {Archive of Formal Proofs},
	author = {Divas{\'o}n, Jose and Kun{\v c}ar, Ond{\v r}ej and Thiemann, Ren{\'e} and Yamada, Akihisa},
	year = {2016},
}
@article{maletzky_hilberts_2019,
	title = {Hilbert's {Nullstellensatz}},
	journal = {Archive of Formal Proofs},
	author = {Maletzky, Alexander},
	year = {2019},
}
@incollection{berardi_locales_2004,
	address = {Heidelberg},
	title = {Locales and {Locale} {Expressions} in {Isabelle}/{Isar}},
	volume = {3085},
	isbn = {978-3-540-22164-7},
	booktitle = {Types for {Proofs} and {Programs}},
	publisher = {Springer},
	author = {Ballarin, Clemens},
	editor = {Berardi, Stefano and Coppo, Mario and Damiani, Ferruccio},
	year = {2004},
	pages = {34--50},
}
@book{ballarin_isabellehol_2020,
	title = {The {Isabelle}/{HOL} {Algebra} {Library}},
	url = {https://isabelle.in.tum.de/website-Isabelle2020/dist/library/HOL/HOL-Algebra/document.pdf},
	editor = {Ballarin, Clemens},
	year = {2020},
}
@misc{noauthor_isabellehol_2020,
	title = {Isabelle/{HOL} {Standard} {Library}},
	url = {https://isabelle.in.tum.de/website-Isabelle2020/dist/library/HOL/HOL/index.html},
	journal = {Isabelle/HOL},
	year = {2020},
}
@misc{noauthor_isabellehol_2020-1,
	title = {Isabelle/{HOL} {Analysis}},
	url = {https://isabelle.in.tum.de/website-Isabelle2020/dist/library/HOL/HOL-Analysis/index.html},
	journal = {Isabelle/HOL},
	year = {2020},
}
@incollection{gonthier_lifting_2013,
	address = {Heidelberg},
	title = {Lifting and {Transfer}: {A} {Modular} {Design} for {Quotients} in {Isabelle}/{HOL}},
	volume = {8307},
	isbn = {978-3-319-03545-1},
	booktitle = {Certified {Programs} and {Proofs}},
	publisher = {Springer},
	author = {Huffman, Brian and Kun{\v c}ar, Ond{\v r}ej},
	editor = {Gonthier, Georges and Norrish, Michael},
	year = {2013},
	pages = {131--146},
}
@incollection{altenkirch_constructive_2007,
	address = {Heidelberg},
	title = {Constructive {Type} {Classes} in {Isabelle}},
	volume = {4502},
	isbn = {978-3-540-74464-1},
	booktitle = {Types for {Proofs} and {Programs}},
	publisher = {Springer},
	author = {Haftmann, Florian and Wenzel, Makarius},
	editor = {Altenkirch, Thorsten and McBride, Conor},
	year = {2007},
	pages = {160--174},
}
@article{ballarin_locales_2014,
	title = {Locales: {A} {Module} {System} for {Mathematical} {Theories}},
	volume = {52},
	number = {2},
	journal = {Journal of Automated Reasoning},
	author = {Ballarin, Clemens},
	year = {2014},
	pages = {123--153},
}
@incollection{kaufmann_mechanized_2010,
	address = {Heidelberg},
	title = {A {Mechanized} {Translation} from {Higher}-{Order} {Logic} to {Set} {Theory}},
	volume = {6172},
	isbn = {978-3-642-14051-8},
	booktitle = {Interactive {Theorem} {Proving}},
	publisher = {Springer},
	author = {Krauss, Alexander and Schropp, Andreas},
	editor = {Kaufmann, Matt and Paulson, Lawrence C.},
	year = {2010},
	pages = {323--338},
}
@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},
}
@incollection{bertot_isar_1999,
	address = {Heidelberg},
	title = {Isar {\textemdash} {A} {Generic} {Interpretative} {Approach} to {Readable} {Formal} {Proof} {Documents}},
	volume = {1690},
	isbn = {978-3-540-66463-5},
	booktitle = {Theorem {Proving} in {Higher} {Order} {Logics}},
	publisher = {Springer},
	author = {Wenzel, Markus},
	editor = {Bertot, Yves and Dowek, Gilles and Th{\'e}ry, Laurent and Hirschowitz, Andr{\'e} and Paulin-Mohring, Christine},
	year = {1999},
	pages = {167--183},
}
@article{wenzel_isabelleisar_2007,
	title = {Isabelle/{Isar} {\textemdash} a {Generic} {Framework} for {Human}-{Readable} {Proof} {Documents}},
	volume = {10},
	number = {23},
	journal = {Studies in Logic, Grammar and Rhetoric},
	author = {Wenzel, Makarius},
	year = {2007},
	pages = {277--297},
}
@incollection{kauers_context_2007,
	address = {Heidelberg},
	title = {Context {Aware} {Calculation} and {Deduction}: {Ring} {Equalities} {Via} {Gr{\"o}bner} {Bases} in {Isabelle}},
	volume = {4573},
	isbn = {978-3-540-73083-5},
	booktitle = {Towards {Mechanized} {Mathematical} {Assistants}},
	publisher = {Springer},
	author = {Chaieb, Amine and Wenzel, Makarius},
	editor = {Kauers, Manuel and Kerber, Manfred and Miner, Robert and Windsteiger, Wolfgang},
	year = {2007},
	pages = {27--39},
}
@inproceedings{lammich_automatic_2013,
	address = {Heidelberg},
	title = {Automatic {Data} {Refinement}},
	isbn = {978-3-642-39634-2},
	booktitle = {Interactive {Theorem} {Proving}},
	publisher = {Springer},
	author = {Lammich, Peter},
	editor = {Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David},
	year = {2013},
	keywords = {Automatic Data, Executable Code, Side Condition, Synthesis Problem, Type Constructor},
	pages = {84--99},
}
@article{kuncar_types_2019,
	title = {From {Types} to {Sets} by {Local} {Type} {Definition} in {Higher}-{Order} {Logic}},
	volume = {62},
	number = {2},
	journal = {Journal of Automated Reasoning},
	author = {Kun{\v c}ar, Ond{\v r}ej and Popescu, Andrei},
	year = {2019},
	pages = {237--260},
}
@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)},
}
@inproceedings{kammuller_locales_1999,
	address = {Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Locales {A} {Sectioning} {Concept} for {Isabelle}},
	isbn = {978-3-540-48256-7},
	booktitle = {Theorem {Proving} in {Higher} {Order} {Logics}},
	publisher = {Springer},
	author = {Kamm{\"u}ller, Florian and Wenzel, Markus and Paulson, Lawrence C.},
	editor = {Bertot, Yves and Dowek, Gilles and Th{\'e}ry, Laurent and Hirschowitz, Andr{\'e} and Paulin-Mohring, Christine},
	year = {1999},
	pages = {149--165},
}
@misc{immler_re_2019,
	title = {Re: [isabelle] {Several} questions in relation to a use case for "types to sets"},
	url = {https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-January/msg00072.html},
	journal = {The Cl-isabelle-users Archives},
	author = {Immler, Fabian},
	year = {2019},
}
@incollection{wenzel_type_1997,
	address = {Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Type {Classes} and {Overloading} in {Higher}-{Order} {Logic}},
	isbn = {978-3-540-69526-4},
	booktitle = {Theorem {Proving} in {Higher} {Order} {Logics}},
	publisher = {Springer},
	author = {Wenzel, Markus},
	editor = {Gunter, Elsa L. and Felty, Amy P.},
	year = {1997},
	keywords = {Type Constructor, Class Definition, Deductive System, Type Class, Type Definition},
	pages = {307--322},
}
@incollection{nipkow_type_1991,
	address = {Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Type {Classes} and {Overloading} {Resolution} via {Order}-{Sorted} {Unification}},
	volume = {523},
	isbn = {978-3-540-47599-6},
	booktitle = {Functional {Programming} {Languages} and {Computer} {Architecture}},
	publisher = {Springer},
	author = {Nipkow, Tobias and Snelting, Gregor},
	editor = {Hughes, John},
	year = {1991},
	pages = {1--14},
}
@article{milehins_conditional_2021,
	title = {Conditional {Transfer} {Rule}},
	journal = {Archive of Formal Proofs},
	author = {Milehins, Mihails},
	year = {2021},
}
@article{kappelmann_speccheck_2021,
	title = {{SpecCheck} - {Specification}-{Based} {Testing} for {Isabelle}/{ML}},
	journal = {Archive of Formal Proofs},
	author = {Kappelmann, Kevin and Bulwahn, Lukas and Willenbrink, Sebastian},
	year = {2021},
}
@book{cain_nine_2019,
	address = {Lisbon},
	title = {Nine {Chapters} on the {Semigroup} {Art}},
	author = {Cain, Alan J},
	year = {2019},
}