Initial commit

1 files changed, 22 insertions, 0 deletions

diff --git a/bib.bib b/bib.bib
new file mode 100755
index 0000000..aa72a8e
--- /dev/null
+++ b/bib.bib
@@ -0,0 +1,22 @@
+@inproceedings{Gregoire-Leroy-02,
+  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}
+}