summaryrefslogtreecommitdiff
path: root/bib.bib
diff options
context:
space:
mode:
authorGuillermo Ramos2015-07-16 01:43:11 +0200
committerGuillermo Ramos2015-07-16 02:27:16 +0200
commit40cf6d0a630c12c52ba9a115dff3e67cea63a31e (patch)
tree4138c6607651cd0aca2c1466054e89460730abfb /bib.bib
parentb1c29f728b7285d51ac121af909f8348ba68a999 (diff)
downloadtfm-40cf6d0a630c12c52ba9a115dff3e67cea63a31e.tar.gz
Fixed problems with bib and Makefile
Diffstat (limited to 'bib.bib')
-rwxr-xr-xbib.bib29
1 files changed, 28 insertions, 1 deletions
diff --git a/bib.bib b/bib.bib
index aa72a8e..8a7ee49 100755
--- a/bib.bib
+++ b/bib.bib
@@ -1,4 +1,15 @@
-@inproceedings{Gregoire-Leroy-02,
+@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{GregoireLeroy02,
author = {Benjamin Gr{\'e}goire and Xavier Leroy},
title = {A compiled implementation of strong reduction},
booktitle = {International Conference on Functional Programming 2002},
@@ -19,4 +30,20 @@ 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},
+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}
}