@article{Shoup04,
  author    = {Victor Shoup},
  title     = {Sequences of games: a tool for taming complexity in security
               proofs},
  journal   = {IACR Cryptology ePrint Archive},
  volume    = 2004,
  year      = 2004,
  pages     = 332,
  ee        = {http://eprint.iacr.org/2004/332},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{BartheGHB11,
  author    = {Gilles Barthe and
               Benjamin Gr{\'e}goire and
               Sylvain Heraud and
               Santiago Zanella B{\'e}guelin},
  title     = {Computer-Aided Security Proofs for the Working Cryptographer},
  booktitle = {CRYPTO},
  year      = {2011},
  pages     = {71-90},
  ee        = {http://dx.doi.org/10.1007/978-3-642-22792-9_5},
  crossref  = {DBLP:conf/crypto/2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/crypto/2011,
  editor    = {Phillip Rogaway},
  title     = {Advances in Cryptology - CRYPTO 2011 - 31st Annual Cryptology
               Conference, Santa Barbara, CA, USA, August 14-18, 2011.
               Proceedings},
  booktitle = {CRYPTO},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6841},
  year      = {2011},
  isbn      = {978-3-642-22791-2},
  ee        = {http://dx.doi.org/10.1007/978-3-642-22792-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{BartheGB09,
  author    = {Gilles Barthe and
               Benjamin Gr{\'e}goire and
               Santiago Zanella B{\'e}guelin},
  title     = {Formal certification of code-based cryptographic proofs},
  booktitle = {POPL},
  year      = {2009},
  pages     = {90-101},
  ee        = {http://doi.acm.org/10.1145/1480881.1480894},
  crossref  = {DBLP:conf/popl/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/popl/2009,
  editor    = {Zhong Shao and
               Benjamin C. Pierce},
  title     = {Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on
               Principles of Programming Languages, POPL 2009, Savannah,
               GA, USA, January 21-23, 2009},
  booktitle = {POPL},
  publisher = {ACM},
  year      = {2009},
  isbn      = {978-1-60558-379-2},
  ee        = {http://dl.acm.org/citation.cfm?id=1480881},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{GoldwasserM84,
  author    = {Shafi Goldwasser and
               Silvio Micali},
  title     = {Probabilistic Encryption},
  journal   = {J. Comput. Syst. Sci.},
  volume    = {28},
  number    = {2},
  year      = {1984},
  pages     = {270-299},
  ee        = {http://dx.doi.org/10.1016/0022-0000(84)90070-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@Article{Shannon49,
  author =       "Claude E. Shannon",
  title =        "Communication Theory of Secrecy Systems",
  journal =      {The Bell System Technical Journal},
  volume =       "28",
  number =       "4",
  pages =        "656--715",
  month =        oct,
  year =         "1949",
  CODEN =        "BSTJAN",
  ISSN =         "0005-8580",
  MRclass =      "60.0X",
  MRnumber =     "0032133 (11,258d)",
  MRreviewer =   "J. L. Doob",
  bibdate =      "Tue Nov 9 11:15:54 MST 2010",
  bibsource =    "http://bstj.bell-labs.com/oldfiles/year.1949/BSTJ.1949.2804.html;
                 http://www.math.utah.edu/pub/bibnet/authors/s/shannon-claude-elwood.bib;
                 http://www.math.utah.edu/pub/tex/bib/bstj1940.bib;
                 http://www.math.utah.edu/pub/tex/bib/cryptography.bib",
  URL =          "http://bstj.bell-labs.com/BSTJ/images/Vol28/bstj28-4-656.pdf;
                 http://en.wikipedia.org/wiki/Communication_Theory_of_Secrecy_Systems;
                 http://www.cs.ucla.edu/~jkong/research/security/shannon1949.pdf",
  acknowledgement = ack-nhfb,
  attnote =      "Included in Part A.",
  author-dates = "Claude Elwood Shannon (April 30, 1916--February 24,
                 2001)",
  fjournal =     "The Bell System Technical Journal",
  journal-URL =  "http://onlinelibrary.wiley.com/journal/10.1002/(ISSN)1538-7305/issues/",
  remark =       "The Wikipedia entry credits this paper as the
                 foundation of modern cryptography.",
}
@Misc{Sorensen98,
    author = {Morten Heine B. Sørensen and Pawel Urzyczyn},
    title = {Lectures on the Curry-Howard Isomorphism},
    year = {1998}
}
@article{Church40,
  author = {A. Church},
  title = {A formulation of a simple theory of types},
  journal = {Journal of Symbolic Logic},
  year = {1940},
  volume = {5},
  pages = {56--68},
  note = {http://www.jstor.org/stable/2266866Electronic Edition},
  url = {http://www.jstor.org/stable/2266866}
}