Date: Tue, 29 Jul 2003 18:09:17 -0700 (PDT) From: David Wagner <daw@cs.berkeley.edu> Subject: Re: POPL Draft Review Message-id: <200307300109.h6U19HZ22596@mozart.cs.berkeley.edu> I have only a few small comments on yoru POPL submission (I know this is too late to be useful, but here they are anyway). Sec 2.1, fourth para: I didn't understand the parenthetical remark "(Note that it is not sufficient ..." What was that saying? Fig 2: at line 4, you have the type "r_t: disp r_x". I'm not sure I understood how the dependent type system works. what if, after line 4, the value of r_x changes to something with a different type? does your type system "remember" to invalidate the type of r_t? maybe you already took care of this -- I don't know enough type theory to be able to tell Sec 3.1, fourth para: The last two sentences were very confusing. I think you need a careful definition of what you mean by "deterministic" transition relation and which relations qualify. I'm not sure this is a realistic assumption, either. It seems plausible that in some cases we could enter a state where we have not already violated the security property but from where a future violation is inevitable. Also, I note that your notion of a "deterministic" relation means that you are not checking a safety property; you are checking some kind of liveness property, which seems a little weird (particularly when you use the word "safety" to describe it). I haven't worked out the implications of this "deterministic" assumption in my head yet, but it stood out at me. I don't have any comments on the more technical parts of the paper -- I didn't have the time to give them the time they deserved. Sorry. Overall, I did find the paper interesting, though.
This archive was generated by hypermail 2b30 : 08/25/03 PDT