2 lutego 2017 14:00
Klara Zielińska: Generalized Refocusing and its formalization in Coq
We report on 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 (where grammars of reduction contexts have multiple context non-terminal symbols) as well as uniform strategies (where the grammars have only one such symbol) handled by the original refocusing method. The resulting machines are proved to correctly implement the reduction strategies of the input semantics. The procedure and the correctness proofs have been formalized in the Coq proof system.