prev Week 7 of 16 next
Since our meeting with Christian Skalka, I've been working on defining the operational semantics (evaluation rules) of our programming language. This requires defining free variables, variable substitutions and proving some results about them. Once I have that down, I can work on proving preservation of types. Types are preserved if when you take one evaluation step from a term e of type T, then the resulting term e' also is of type T. Brigitte tells me that writing out a proof of preservation will give us valuable insight about whether the terms and types we've defined so far express what we really intend.
As part of this work, I took a closer look at our "box" connective and its introduction and elimination rules. In doing so, I worked out some new, interesting examples that helped me understand the finer details of how the box connective works and what it may be used for. This was crucial, since I never felt quite comfortable with the introduction rule Brigitte proposed, but now I have a better intuition about it. For example, I played around with functions that take in a boxed expression and change its permission requirements. This allowed me to observe under what conditions such an operation can be performed: the old permission requirements must be derivable from the new permission requirements in the authorization logic. I think this bit of exploration will help me define free variables correctly. In any case, the examples I looked at are interesting enough for me to expand on and include in my final report.
After the preservation proof is worked out, I intend to encode stack inspection in our system, as suggested. Also, Skalka sent us links to some papers that look quite promising. I intend to read them soon, but have only skimmed them so far. I'm looking forward to it, though.