A Simple Application of Lightweight Fusion to Proving the Equivalence of Abstract Machines

Olivier Danvy, Kevin Millikin

    Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearch

    Abstract

    We show how Ohori and Sasano's recent lightweight fusion by fixed-point promotion provides a simple way to prove the equivalence of the two standard styles of specification of abstract machines: (1) as a transition function together with a `driver loop' implementing the iteration of this transition function; and (2) as a function directly iterating upon a configuration until reaching a final state, if ever. The equivalence hinges on the fact that the latter style of specification is a fused version of the former one. The need for such a simple proof is motivated by our recent work on syntactic correspondences between reduction semantics and abstract machines, using refocusing
    Original languageEnglish
    Book seriesB R I C S Report Series
    IssueRS-07-8
    Number of pages6
    ISSN0909-0878
    Publication statusPublished - 2007

    Fingerprint

    Dive into the research topics of 'A Simple Application of Lightweight Fusion to Proving the Equivalence of Abstract Machines'. Together they form a unique fingerprint.

    Cite this