@string{JCS =  "Journal of Computer Security"}
@string{PUB-IEEE = {IEEE Computer Society}}
@string{PUB-MIT     = {MIT Press}}
@STRING{LNCS =   {Lecture Notes in Computer Science}}
@string{PUB-SV      = {Springer}}


@inproceedings{HuntSands:POPL2006,
  author    = {Sebastian Hunt and
               David Sands},
  title     = {On flow-sensitive security types.},
  pages     = {79-90},
  ee        = {http://doi.acm.org/10.1145/1111037.1111045},
  crossref  = {DBLP:conf/popl/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/popl/2006,
  editor    = {J. Gregory Morrisett and Simon L. {Peyton Jones}},
  title     = {Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on
               Principles of Programming Languages (POPL 2006)},
  booktitle = {Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on
               Principles of Programming Languages (POPL 2006)},
  location  = {Charleston, South Carolina},
  date      = {January 11-13, 2006},
  publisher = {ACM Press},
  year      = {2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{BeringerHofmann:CSF2007,
  author =       {Lennart Beringer and Martin Hofmann},
  title =        {Secure information flow and program logics},
  booktitle =    {Proceedings of the 20th IEEE Computer Security Foundations Symposium (CSF 2007)},
  publisher =    PUB-IEEE,
  year =         2007,
  pages =        {233--248}
}

@book{Winskel93,
  author = {Glynn Winskel},
  title = {The formal semantics of programming languages, an introduction},
  publisher = PUB-MIT,
  year = 1993
}

@phdthesis{KleymannPhD,
  author = {Thomas Kleymann}, 
  title = {Hoare Logic and VDM: Machine-Checked Soundness and Completeness Proofs},
  school = {LFCS, School of Informatics},
  instituion = {University of Edinburgh},
  note = {Technical Report ECS-LFCS-98-392}, 
  month = sep,
  year = 1998
}

@inproceedings{Nipkow-CSL02,
  author={Tobias Nipkow},
  title={Hoare Logics for Recursive Procedures and Unbounded Nondeterminism},
  booktitle={Computer Science Logic (CSL 2002)},
  editor={Julian Bradfield},
  publisher=PUB-SV,
  series=LNCS,
  volume=2471,
  pages={103-119},
  year=2002}
}

@incollection{Nipkow-AFP-AHL,
  author =       {Tobias Nipkow},
  title =        {Abstract {H}oare Logics},
  booktitle =    {Archive of Formal Proofs},
  editor =       {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  publisher =    {\url{http://isa-afp.org/entries/Abstract-Hoare-Logics.shtml}},
  month =        Jun,
  year =         2008,
  note =         {Formal proof development},
}

@article{VolpanoSmithIrvine:JCS1996,
  author =  "Dennis Volpano and Geoffrey Smith and Cynthia Irvine",
  title =  "A Sound Type System for Secure Flow Analysis",
  journal =  JCS,
  volume =  4,
  number =  3,
  year =  1996,
  pages =  "167--187"
}

@article{DBLP:journals/jfp/BanerjeeN05,
  author    = {Anindya Banerjee and
               David A. Naumann},
  title     = {Stack-based access control and secure information flow},
  journal   = {Journal of Functional Programming},
  volume    = {15},
  number    = {2},
  year      = {2005},
  pages     = {131-177},
  ee        = {https://doi.org/10.1017/S0956796804005453},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Misc{MobiusDeliverable2.3,
  author =       {{\sc Mobius} Consortium},
  title =        {Deliverable~2.3: Report on Type Systems},
  year =         2007,
  note =         {Available online from \url{http://mobius.inria.fr}}
}