@article{de2008tensor,
  title={Tensor rank and the ill-posedness of the best low-rank approximation problem},
  author={De Silva, Vin and Lim, Lek-Heng},
  journal={SIAM Journal on Matrix Analysis and Applications},
  volume={30},
  number={3},
  pages={1084--1127},
  year={2008},
  publisher={SIAM}
}

@book{conway2013course,
title={A course in functional analysis},
author={Conway, John B},
volume={96},
year={2013},
publisher={Springer Science \& Business Media}
}

@book{Helemskii,
title={Lectures and Exercises on Functional Analysis},
author={A. Ya. Helemskii},
volume={233},
year={2006},
publisher={Translations of mathematical monographs,
 American Mathematical Society}
}

@book{lang2004algebra,
  title={Algebra, volume 211 of},
  author={Lang, Serge},
  publisher={Graduate Texts in Mathematics},
  year={2004}
}


@book{rolfschneiderminkowskiadd2011,
  author = {Rolf Schneider (originator)},
  title = {Minkowski addition},
  year = {2011},
  url = {http://www.encyclopediaofmath.org/index.php?title=Minkowski_addition&oldid=16121}
}


@article{sokal2011really,
  title={A really simple elementary proof of the uniform boundedness theorem},
  author={Sokal, Alan D},
  journal={The American Mathematical Monthly},
  volume={118},
  number={5},
  pages={450--452},
  year={2011},
  publisher={Taylor \& Francis}
}

@inproceedings{fleuriot2000mechanization,
  title={On the mechanization of real analysis in {Isabelle/HOL}},
  author={Fleuriot, Jacques D},
  booktitle={International Conference on Theorem Proving in Higher Order Logics},
  pages={145--161},
  year={2000},
  organization={Springer}
}

@article{fleuriot2000mechanizing,
  title={Mechanizing nonstandard real analysis},
  author={Fleuriot, Jacques D and Paulson, Lawrence C},
  journal={LMS Journal of Computation and Mathematics},
  volume={3},
  pages={140--190},
  year={2000},
  publisher={Cambridge University Press}
}

@inproceedings{fleuriot2010exploring,
  title={Exploring the foundations of discrete analytical geometry in {Isabelle/HOL}},
  author={Fleuriot, Jacques},
  booktitle={International Workshop on Automated Deduction in Geometry},
  pages={34--50},
  year={2010},
  organization={Springer}
}

@inproceedings{fleuriot2000nonstandard,
  title={Nonstandard geometric proofs},
  author={Fleuriot, Jacques D},
  booktitle={International Workshop on Automated Deduction in Geometry},
  pages={246--267},
  year={2000},
  organization={Springer}
}

@book{fleuriot2012combination,
  title={A combination of geometry theorem proving and nonstandard analysis with application to Newton’s Principia},
  author={Fleuriot, Jacques},
  year={2012},
  publisher={Springer Science \& Business Media}
}

@book{goldblatt2012lectures,
  title={Lectures on the hyperreals: an introduction to nonstandard analysis},
  author={Goldblatt, Robert},
  volume={188},
  year={2012},
  publisher={Springer Science \& Business Media}
}

@misc{code-generation-tutorial,
  title={Code generation from {Isabelle/HOL} theories},
  author={Florian Haftmann},
  year=2019,
  howpublished={\url{https://isabelle.in.tum.de/website-Isabelle2019/dist/Isabelle2019/doc/codegen.pdf}}
}
