1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
|
@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},
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},
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}
}
|
