2026-08-10T13:40:37Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7718 2024-03-06T10:41:02Z ddc:004 open_access

Generalized Refocusing: From Hybrid Strategies to Abstract Machines Biernacka, Malgorzata Charatonik, Witold Zielinska, Klara reduction semantics abstract machines formal verification Coq We present a generalization of the refocusing procedure that provides a generic method for deriving an abstract machine from a specification of a reduction semantics satisfying simple initial conditions. The proposed generalization is applicable to a class of reduction semantics encoding hybrid strategies as well as uniform strategies handled by the original refocusing method. The resulting machine is proved to correctly trace (i.e., bisimulate in smaller steps) the input reduction semantics. The procedure and the correctness proofs have been formalized in the Coq proof assistant. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Malgorzata Biernacka and Witold Charatonik and Klara Zielinska 2017 Is Part Of LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2017.10 urn:nbn:de:0030-drops-77188 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.10 eng https://creativecommons.org/licenses/by/3.0/legalcode