@article{
  R1,
  author={Pasquale Noce},
  title={Noninterference Security in Communicating Sequential Processes},
  journal={Archive of Formal Proofs},
  month=may,
  year=2014,
  note={\url{http://isa-afp.org/entries/Noninterference_CSP.shtml}, Formal proof development},
  ISSN={2150-914x}
}

@article{
  R2,
  author={Pasquale Noce},
  title={The Ipurge Unwinding Theorem for CSP Noninterference Security},
  journal={Archive of Formal Proofs},
  month=jun,
  year=2015,
  note={\url{http://isa-afp.org/entries/Noninterference_Ipurge_Unwinding.shtml}, Formal proof development},
  ISSN={2150-914x}
}

@article{
  R3,
  author={Pasquale Noce},
  title={The Generic Unwinding Theorem for CSP Noninterference Security},
  journal={Archive of Formal Proofs},
  month=jun,
  year=2015,
  note={\url{http://isa-afp.org/entries/Noninterference_Generic_Unwinding.shtml}, Formal proof development},
  ISSN={2150-914x}
}

@article{
  R4,
  author={Pasquale Noce},
  title={The Inductive Unwinding Theorem for CSP Noninterference Security},
  journal={Archive of Formal Proofs},
  month=aug,
  year=2015,
  note={\url{http://isa-afp.org/entries/Noninterference_Inductive_Unwinding.shtml}, Formal proof development},
  ISSN={2150-914x}
}

@article{
  R5,
  author={Pasquale Noce},
  title={Conservation of CSP Noninterference Security under Sequential Composition},
  journal={Archive of Formal Proofs},
  month=apr,
  year=2016,
  note={\url{http://isa-afp.org/entries/Noninterference_Sequential_Composition.shtml}, Formal proof development},
  ISSN={2150-914x}
}

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

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

@manual{
  R8,
  author={Tobias Nipkow},
  title={Programming and Proving in Isabelle/HOL},
  month=feb,
  year=2016,
  note={\url{http://isabelle.in.tum.de/website-Isabelle2016/dist/Isabelle2016/doc/prog-prove.pdf}}
}

@manual{
  R9,
  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{
  R10,
  author={Alexander Krauss},
  title={Defining Recursive Functions in Isabelle/HOL},
  note={\url{http://isabelle.in.tum.de/website-Isabelle2016/dist/Isabelle2016/doc/functions.pdf}}
}
