Automating Derivations of Abstract Machines from Reduction Semantics: A Generic Formalization of Refocusing in Coq

Filip Sieczkowski, Małgorzata Biernacka, Dariusz Biernacki

    Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review

    Abstrakt

    We present a generic formalization of the refocusing trans- formation for functional languages in the Coq proof assistant. The refo- cusing technique, due to Danvy and Nielsen, allows for mechanical trans- formation of an evaluator implementing a reduction semantics into an equivalent abstract machine via a succession of simple program transfor- mations. So far, refocusing has been used only as an informal procedure: the conditions required of a reduction semantics have not been formally captured, and the transformation has not been formally proved correct. The aim of this work is to formalize and prove correct the refocusing technique. To this end, we first propose an axiomatization of reduction semantics that is sufficient to automatically apply the refocusing method. Next, we prove that any reduction semantics conforming to this axiom- atization can be automatically transformed into an abstract machine equivalent to it. The article is accompanied by a Coq development that contains the formalization of the refocusing method and a number of case studies that serve both as an illustration of the method and as a sanity check on the axiomatization.
    OriginalsprogEngelsk
    TitelIFL'10 Proceedings of the 22nd international conference on Implementation and application of functional languages
    Antal sider16
    ForlagSpringer
    Publikationsdato2011
    Sider72-88
    ISBN (Trykt)978-3-642-24275-5
    DOI
    StatusUdgivet - 2011

    Fingeraftryk

    Dyk ned i forskningsemnerne om 'Automating Derivations of Abstract Machines from Reduction Semantics: A Generic Formalization of Refocusing in Coq'. Sammen danner de et unikt fingeraftryk.

    Citationsformater