License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2022.7
URN: urn:nbn:de:0030-drops-167165
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16716/
Biernacka, Małgorzata ;
Charatonik, Witold ;
Drab, Tomasz
The Zoo of Lambda-Calculus Reduction Strategies, And Coq
Abstract
We present a generic framework for the specification and reasoning about reduction strategies in the lambda calculus, representable as sets of term decompositions. It is provided as a Coq formalization that features a novel format of phased strategies. It facilitates concise description and algebraic reasoning about properties of reduction strategies. The formalization accommodates many well-known strategies, both weak and strong, such as call by name, call by value, head reduction, normal order, full β-reduction, etc. We illustrate the use of the framework as a tool to inspect and categorize the "zoo" of existing strategies, as well as to discover and study new ones with particular properties.
BibTeX - Entry
@InProceedings{biernacka_et_al:LIPIcs.ITP.2022.7,
author = {Biernacka, Ma{\l}gorzata and Charatonik, Witold and Drab, Tomasz},
title = {{The Zoo of Lambda-Calculus Reduction Strategies, And Coq}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {7:1--7:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16716},
URN = {urn:nbn:de:0030-drops-167165},
doi = {10.4230/LIPIcs.ITP.2022.7},
annote = {Keywords: Lambda calculus, Reduction strategies, Coq}
}
