2026-07-23T15:38:20Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16716 2024-03-06T10:58:07Z ddc:004 open_access

The Zoo of Lambda-Calculus Reduction Strategies, And Coq Biernacka, Małgorzata Charatonik, Witold Drab, Tomasz Lambda calculus Reduction strategies Coq 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Małgorzata Biernacka and Witold Charatonik and Tomasz Drab 2022 Is Part Of LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2022.7 urn:nbn:de:0030-drops-167165 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.7 eng https://creativecommons.org/licenses/by/4.0/legalcode