@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},
}
@incollection{berardi_local_2009,
	address = {Heidelberg},
	title = {Local {Theory} {Specifications} in {Isabelle}/{Isar}},
	volume = {5497},
	isbn = {978-3-642-02443-6},
	booktitle = {Types for {Proofs} and {Programs}},
	publisher = {Springer},
	author = {Haftmann, Florian and Wenzel, Makarius},
	editor = {Berardi, Stefano and Damiani, Ferruccio and de{\textquoteright}Liguoro, Ugo},
	year = {2009},
	pages = {153--168},
}
@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},
}
@misc{noauthor_isabelle_nodate,
	title = {Isabelle mailing-list},
	url = {https://lists.cam.ac.uk/pipermail/cl-isabelle-users/},
	journal = {The Cl-isabelle-users Archives},
}
@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},
}
@inproceedings{traytel_foundational_2012,
	address = {Dubrovnik},
	title = {Foundational, {Compositional} ({Co})datatypes for {Higher}-{Order} {Logic}: {Category} {Theory} {Applied} to {Theorem} {Proving}},
	booktitle = {27th {Annual} {IEEE} {Symposium} on {Logic} in {Computer} {Science}},
	publisher = {IEEE},
	author = {Traytel, Dmitry and Popescu, Andrei and Blanchette, Jasmin C.},
	year = {2012},
	keywords = {(co)datatypes, Abstracts, bounded natural functor, cardinals, categorical operation, category theory, Category theory, compositional datatype, datatype definition, definitional package, finitely branching tree, formal logic, foundational datatype, fully modular framework, high-level specification, higher-order logic, HOL Light, HOL4, interactive theorem prover, interactive theorem proving, internal datatype construction, Isabelle/HOL, logical primitive, mixed mutual recursion, nested recursion, Semantics, Set theory, Shape, Standards, theorem proving, trees (mathematics)},
	pages = {596--605},
}
@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},
}
@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{blanchette_bindings_2019,
	title = {Bindings as {Bounded} {Natural} {Functors}},
	volume = {3},
	number = {POPL},
	journal = {Proceedings of the ACM on Programming Languages},
	author = {Blanchette, Jasmin Christian and Gheri, Lorenzo and Popescu, Andrei and Traytel, Dmitriy},
	year = {2019},
	pages = {22:1--22:34},
}
@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},
}
@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},
}
@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)},
}
@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},
}
@misc{noauthor_stack_nodate,
	title = {Stack {Exchange}},
	url = {https://stackexchange.com/},
}
@article{milehins_extension_2021,
	title = {Extension of {Types}-{To}-{Sets}},
	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},
}
