To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 14/12/07 - Paris - FR

           Vous pouvez vous abonner à nos annonces de séminaires
                    http://pauillac.inria.fr/seminaires/

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                         Amphi Turing du bâtiment 1

                        Vendredi 14 décembre, 10h30

                               -------------
                               Olivier Danvy
                               -------------

        BRICS, Department of Computer Science, University of Aarhus

                 =========================================
                         On the equivalence between
                 small-step and big-step abstract machines
                          using lightweight fusion
                 =========================================

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) in small-step form, as a
state-transition function together with a `driver loop,' i.e., a function
implementing the iteration of this transition function; and (2) in big-step
form, as a tail-recursive function that directly maps a given configuration to
a final state, if any.  The equivalence hinges on our observation that for
abstract machines, fusing a small-step specification yields a big-step
specification. We illustrate this observation here with a recognizer for Dyck
words, the CEK machine, and Krivine's machine with call/cc.
  
The need for such a simple proof is motivated by our current work on
small-step abstract machines as obtained by refocusing a function implementing
a reduction semantics (a syntactic correspondence), and big-step abstract
machines as obtained by CPS-transforming and then defunctionalizing a function
implementing a big-step semantics (a functional correspondence).

This is joint work with Kevin Millikin.