@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}
}

@article{Krivine07,
year={2007},
issn={1388-3690},
journal={Higher-Order and Symbolic Computation},
volume={20},
number={3},
doi={10.1007/s10990-007-9018-9},
title={A call-by-name lambda-calculus machine},
url={http://dx.doi.org/10.1007/s10990-007-9018-9},
publisher={Springer US},
keywords={Lambda-calculus machine; Control instruction; Curry-Howard correspondence},
author={Krivine, Jean-Louis},
pages={199-207},
language={English}
}

@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 = "36th ACM SIGPLAN-SIGACT Symposium on
               Principles of Programming Languages, POPL 2009",
  publisher = "ACM",
  year      = "2009",
  pages     = "90-101",
  url       = "http://dx.doi.org/10.1145/1480881.1480894"
}


@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}
}

@incollection{BartheGB12,
year={2012},
isbn={978-3-642-31112-3},
booktitle={Mathematics of Program Construction},
volume={7342},
series={Lecture Notes in Computer Science},
editor={Gibbons, Jeremy and Nogueira, Pablo},
doi={10.1007/978-3-642-31113-0_1},
title={Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs},
url={http://dx.doi.org/10.1007/978-3-642-31113-0_1},
publisher={Springer Berlin Heidelberg},
author={Barthe, Gilles and Grégoire, Benjamin and Zanella Béguelin, Santiago},
pages={1-6},
language={English}
}


@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}
}

 [download]

@inproceedings{LeroyG02,
 author = {Gr{\'e}goire, Benjamin and Leroy, Xavier},
 title = {A Compiled Implementation of Strong Reduction},
 booktitle = {Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming},
 series = {ICFP '02},
 year = {2002},
 isbn = {1-58113-487-8},
 location = {Pittsburgh, PA, USA},
 pages = {235--246},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/581478.581501},
 doi = {10.1145/581478.581501},
 acmid = {581501},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Coq, abstract machine, beta-equivalence, calculus of constructions, normalization by evaluation, strong reduction, virtual machine},
}

@article{Douence07,
 author = {Douence, R{\'e}mi and Fradet, Pascal},
 title = {The Next 700 Krivine Machines},
 journal = {Higher Order Symbol. Comput.},
 issue_date = {September 2007},
 volume = {20},
 number = {3},
 month = sep,
 year = {2007},
 issn = {1388-3690},
 pages = {237--255},
 numpages = {19},
 url = {http://dx.doi.org/10.1007/s10990-007-9016-y},
 doi = {10.1007/s10990-007-9016-y},
 acmid = {1325151},
 publisher = {Kluwer Academic Publishers},
 address = {Hingham, MA, USA},
 keywords = {Abstract machines, Compilation, Functional language implementations, Krivine machine, Program transformation},
}

@incollection{Sestoft02,
 author = {Sestoft, Peter},
 chapter = {Demonstrating Lambda Calculus Reduction},
 title = {The Essence of Computation},
 editor = {Mogensen, Torben \AE and Schmidt, David A. and Sudborough, I. Hal},
 year = {2002},
 isbn = {3-540-00326-6},
 pages = {420--435},
 numpages = {16},
 url = {http://dl.acm.org/citation.cfm?id=860256.860276},
 acmid = {860276},
 publisher = {Springer-Verlag New York, Inc.},
 address = {New York, NY, USA},
}

@article{Church36,
  added-at = {2010-06-28T20:17:37.000+0200},
  author = {Church, Alonzo},
  biburl = {http://www.bibsonomy.org/bibtex/29be3cded6900817f0c47b90e220033ce/mhwombat},
  citeulike-article-id = {843319},
  citeulike-linkout-0 = {http://dx.doi.org/10.2307/2371045},
  citeulike-linkout-1 = {http://www.jstor.org/stable/2371045},
  doi = {10.2307/2371045},
  groups = {public},
  interhash = {1eae6974a9400cddb30164e1d09e030b},
  intrahash = {414fd23bcd903e33a391dea42b19d7df},
  issn = {00029327},
  journal = {American Journal of Mathematics},
  keywords = {elementary_number_theory mathematics},
  month = {April},
  number = 2,
  pages = {345--363},
  posted-at = {2010-06-26 08:13:09},
  priority = {2},
  timestamp = {2011-06-01T23:55:28.000+0200},
  title = {An Unsolvable Problem of Elementary Number Theory},
  url = {http://dx.doi.org/10.2307/2371045},
  username = {mhwombat},
  volume = 58,
  year = 1936
}

@techreport{Leroy90,
  author = {Xavier Leroy},
  title = {The {ZINC} experiment: an economical
                         implementation of the {ML} language},
  institution = {INRIA},
  type = {Technical report},
  number = {117},
  year = {1990},
  urllocal = {http://gallium.inria.fr/~xleroy/publi/ZINC.pdf},
  abstract = {This report details the design and implementation of the ZINC
system.  This is an experimental implementation of the ML
language, which has later evolved in the Caml Light system.
This system is strongly oriented toward separate compilation
and the production of small, standalone programs; type safety
is ensured by a Modula-2-like module system.  ZINC uses
simple, portable techniques, such as bytecode interpretation;
a sophisticated execution model helps counterbalance the
interpretation overhead.},
  xtopic = {caml}
}

@book{PeytonJones87,
 author = {Peyton Jones, Simon L.},
 title = {The Implementation of Functional Programming Languages (Prentice-Hall International Series in Computer Science)},
 year = {1987},
 isbn = {013453333X},
 publisher = {Prentice-Hall, Inc.},
 address = {Upper Saddle River, NJ, USA},
}

@incollection{Mogensen00,
year={2000},
isbn={978-3-540-67102-2},
booktitle={Perspectives of System Informatics},
volume={1755},
series={Lecture Notes in Computer Science},
editor={Bjøner, Dines and Broy, Manfred and Zamulin, AlexandreV.},
doi={10.1007/3-540-46562-6_11},
title={Linear Time Self-Interpretation of the Pure Lambda Calculus},
url={http://dx.doi.org/10.1007/3-540-46562-6_11},
publisher={Springer Berlin Heidelberg},
author={Mogensen, TorbenÆ.},
pages={128-142},
language={English}
}

@article{Coquand88,
 author = {Coquand, Thierry and Huet, Gerard},
 title = {The Calculus of Constructions},
 journal = {Inf. Comput.},
 issue_date = {February/March 1988},
 volume = {76},
 number = {2-3},
 month = feb,
 year = {1988},
 issn = {0890-5401},
 pages = {95--120},
 numpages = {26},
 url = {http://dx.doi.org/10.1016/0890-5401(88)90005-3},
 doi = {10.1016/0890-5401(88)90005-3},
 acmid = {47725},
 publisher = {Academic Press, Inc.},
 address = {Duluth, MN, USA},
}

@book{Baader98,
 author = {Baader, Franz and Nipkow, Tobias},
 title = {Term Rewriting and All That},
 year = {1998},
 isbn = {0-521-45520-0},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
}