search

jstolarek / slicer

Companion code for paper "Imperative Functional Programs that Explain their Work", Wilmer Ricciotti, Jan Stolarek, Roly Perera and James Cheney, ICFP 2017, Oxford, UK
http://dl.acm.org/citation.cfm?id=3110258
GNU General Public License v3.0
6 stars 0 forks source link

leq/lub definitions for store labels #42

Closed jstolarek closed 7 years ago

jstolarek commented 7 years ago

I'm writing the definitions of lub and leq for new tracing constructs:

           | TRef (Maybe StoreLabel) Trace | TDeref (Maybe StoreLabel) Trace
           | TAssign (Maybe StoreLabel) Trace Trace

I wonder what to do with store labels. I think guarding to ensure they are identical is the right thing to do.

rolyp commented 7 years ago

That sounds right.

On 22 February 2017 at 21:33, Jan Stolarek notifications@github.com wrote:

I'm writing the definitions of lub and leq for new tracing constructs:

       | TRef (Maybe StoreLabel) Trace | TDeref (Maybe StoreLabel) Trace
       | TAssign (Maybe StoreLabel) Trace Trace

I wonder what to do with store labels. I think guarding to ensure they are identical is the right thing to do.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/jstolarek/slicer/issues/42, or mute the thread https://github.com/notifications/unsubscribe-auth/AAHY8jPLIm0WMAnOnOHn0ke9-Whxvv-aks5rfKm9gaJpZM4MJN5Z .