19/06/15, sent for revision

1 files changed, 173 insertions, 22 deletions

diff --git a/bib.bib b/bib.bib
index 8a7ee49..ed7095e 100644
--- a/bib.bib
+++ b/bib.bib
@@ -9,28 +9,6 @@
   ee        = {http://eprint.iacr.org/2004/332},
   bibsource = {DBLP, http://dblp.uni-trier.de}
 }
-@inproceedings{GregoireLeroy02,
-  author = {Benjamin Gr{\'e}goire and Xavier Leroy},
-  title = {A compiled implementation of strong reduction},
-  booktitle = {International Conference on Functional Programming 2002},
-  pages = {235--246},
-  publisher = {ACM Press},
-  year = 2002,
-  urllocal = {http://gallium.inria.fr/~xleroy/publi/strong-reduction.pdf},
-  urlpublisher = {http://dx.doi.org/10.1145/581478.581501},
-  abstract = {Motivated by applications to proof assistants based on dependent
-types, we develop and prove correct a strong reducer and
-$\beta$-equivalence checker for the $\lambda$-calculus with products,
-sums, and guarded fixpoints.  Our approach is based on compilation to
-the bytecode of an abstract machine performing weak reductions on
-non-closed terms, derived with minimal modifications from the ZAM
-machine used in the Objective Caml bytecode interpreter, and
-complemented by a recursive ``read back'' procedure.  An
-implementation in the Coq proof assistant demonstrates important
-speed-ups compared with the original interpreter-based implementation
-of strong reduction in Coq.},
-  xtopic = {caml}
-},
 
 @article{Krivine07,
 year={2007},
@@ -47,3 +25,176 @@ 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}
+}
\ No newline at end of file