%0 Conference Paper %1 gregoire %A Grégoire, Benjamin %A Leroy, Xavier %B International Conference on Functional Programming 2002 %D 2002 %I ACM Press %K imported %P 235-246 %T A compiled implementation of strong reduction %U /brokenurl#http://gallium.inria.fr/~xleroy/publi/strong-reduction.pdf %X Motivated by applications to proof assistants based on dependent types, we develop and prove correct a strong reducer and $\beta$-equivalence checker for the $łambda$-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.

@inproceedings{gregoire, 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.}}, added-at = {2010-08-25T08:47:38.000+0200}, author = {Gr{\'{e}}goire, Benjamin and Leroy, Xavier}, biburl = {https://www.bibsonomy.org/bibtex/21d2f6bf52112bb446b12d54a21c49f47/miguel.pagano}, booktitle = {{International Conference on Functional Programming 2002}}, interhash = {a3ce8b01b84d4a64f541459db8ed97fa}, intrahash = {1d2f6bf52112bb446b12d54a21c49f47}, keywords = {imported}, pages = {235-246}, publisher = {{ACM Press}}, timestamp = {2010-08-25T08:47:40.000+0200}, title = {{A compiled implementation of strong reduction}}, url = {/brokenurl#{http://gallium.inria.fr/~xleroy/publi/strong-reduction.pdf}}, urlpublisher = {{http://doi.acm.org/10.1145/581478.581501}}, xtopic = {{caml}}, year = {{2002}} }