@book{
  R1,
  author={C. A. R. Hoare},
  title={Communicating Sequential Processes},
  publisher={Prentice-Hall, Inc.},
  year=1985
}

@inproceedings{
  R2,
  author={J. A. Goguen and J. Meseguer},
  title={Security Policies and Security Models},
  booktitle={IEEE Symposium on Security and Privacy},
  year=1982
}

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

@inproceedings{
  R4,
  author={Daryl McCullough},
  title={Noninterference and the Composability of Security Properties},
  booktitle={Proceedings of the 1988 IEEE Conference on Security and Privacy},
  year=1988,
}

@manual{
  R5,
  author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
  title={Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  month=dec,
  year=2013,
  note={\url{http://isabelle.in.tum.de/website-Isabelle2013-2/dist/Isabelle2013-2/doc/tutorial.pdf}}
}

@manual{
  R6,
  author={Tobias Nipkow},
  title={Programming and Proving in Isabelle/HOL},
  month=dec,
  year=2013,
  note={\url{http://isabelle.in.tum.de/website-Isabelle2013-2/dist/Isabelle2013-2/doc/prog-prove.pdf}}
}

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

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