diff options
author | Guillermo Ramos | 2015-07-16 01:43:11 +0200 |
---|---|---|
committer | Guillermo Ramos | 2015-07-16 02:27:16 +0200 |
commit | 40cf6d0a630c12c52ba9a115dff3e67cea63a31e (patch) | |
tree | 4138c6607651cd0aca2c1466054e89460730abfb /bib.bib | |
parent | b1c29f728b7285d51ac121af909f8348ba68a999 (diff) | |
download | tfm-40cf6d0a630c12c52ba9a115dff3e67cea63a31e.tar.gz |
Fixed problems with bib and Makefile
Diffstat (limited to 'bib.bib')
-rwxr-xr-x | bib.bib | 29 |
1 files changed, 28 insertions, 1 deletions
@@ -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} } |