@book {
  Nipkow23-1,
  author = {Tobias Nipkow and Gerwin Klein},
  title = {{Concrete Semantics with Isabelle/HOL}},
  month = feb,
  year = 2023,
  publisher = {Springer-Verlag},
  note = {(Current version: \url{http://www.concrete-semantics.org/concrete-semantics.pdf})}
}

@misc {
  Nipkow23-2,
  author = {Tobias Nipkow and Gerwin Klein},
  title = {{Theory HOL-IMP.Sec\_Type\_Expr (included in the Isabelle2023 distribution)}},
  note = {\url{https://isabelle.in.tum.de/website-Isabelle2023/dist/library/HOL/HOL-IMP/Sec\_Type\_Expr.html}}
}

@misc {
  Nipkow23-3,
  author = {Tobias Nipkow and Gerwin Klein},
  title = {{Theory HOL-IMP.Sec\_TypingT (included in the Isabelle2023 distribution)}},
  note = {\url{https://isabelle.in.tum.de/website-Isabelle2023/dist/library/HOL/HOL-IMP/Sec\_TypingT.html}}
}

@techreport {
  Rushby92,
  author = {John Rushby},
  title = {{Noninterference, Transitivity, and Channel-Control Security Policies}},
  institution = {{SRI International}},
  month = dec,
  year = 1992
}

@article {
  Volpano96,
  author = {Dennis Volpano and Geoffrey Smith and Cynthia Irvine},
  title = {{A Sound Type System for Secure Flow Analysis}},
  journal = {Journal of Computer Security},
  month = jan,
  year = 1996
}

@inproceedings {
  Volpano97,
  author = {Dennis Volpano and Geoffrey Smith},
  title = {{Eliminating Covert Flows with Minimum Typings}},
  booktitle = {{Proc. 10th IEEE Computer Security Foundations Workshop}},
  month = jun,
  year = 1997
}

@manual {
  Paulson23,
  author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title = {{Isabelle/HOL -- A Proof Assistant for Higher-Order Logic}},
  month = sep,
  year = 2023,
  note = {\url{https://isabelle.in.tum.de/website-Isabelle2023/dist/Isabelle2023/doc/tutorial.pdf}}
}

@manual {
  Nipkow23-4,
  author = {Tobias Nipkow},
  title = {{Programming and Proving in Isabelle/HOL}},
  month = sep,
  year = 2023,
  note = {\url{https://isabelle.in.tum.de/website-Isabelle2023/dist/Isabelle2023/doc/prog-prove.pdf}}
}

@manual {
  Krauss23,
  author = {Alexander Krauss},
  title = {{Defining Recursive Functions in Isabelle/HOL}},
  note = {\url{https://isabelle.in.tum.de/website-Isabelle2023/dist/Isabelle2023/doc/functions.pdf}}
}

@manual {
  Nipkow11,
  author = {Tobias Nipkow},
  title = {{A Tutorial Introduction to Structured Isar Proofs}},
  note = {\url{https://isabelle.in.tum.de/website-Isabelle2011/dist/Isabelle2011/doc/isar-overview.pdf}}
}

@manual {
  Ballarin23,
  author = {Clemens Ballarin},
  title = {{Tutorial to Locales and Locale Interpretation}},
  note = {\url{https://isabelle.in.tum.de/website-Isabelle2023/dist/Isabelle2023/doc/locales.pdf}}
}
