[L7] ================================================ AMAST Links 02 06

         Note: rewrite semantics for extension of mu-calculus 
                    based on continuation semantics
                           Thomas Streicher

   The full version of this information is available at URL:
   http://www.cs.utwente.nl/data/amast/links/v02/i06/full/AC0206L7.txt

  In this note I show how to give a continuation semantics to an 
extension of Parigot's mu-calculus from which there follows a simple 
equational presentation and rewrite semantics. Though I have had the 
semantics since quite a time the idea to use it for extending 
mu-calculus and deriving a nice rewrite semantics for it from this 
semantics came to me during a talk of Philippe Audebaud during his talk
at the Scott conference in Darmstadt this spring/summer.  I don't 
precisely remember his presentation, so I cannot compare what's below 
with his work; but it looks simpler to me than what I remember to have 
seen in the talk. Maybe Philippe has some further equations to 
guarantee confluence or things like that. I personally haven't checked 
confluence myself. But it is clear that the machine computations of an 
extended Krivine's machine are reflected one-to-one by rewrite 
derivations in the calculus below.  Anyway the semantic justification 
of the rewrite rules may be of interest and facilitate understanding 
of the calculus.