I read through the paper, and made the following notes. Hopefully you find them useful.
In 5. of Definition 2.1.4, we read βββ₯0β. Is this different from just βββ? You freely use βββ in 5. of definition 2.2.1.
The letter πΎ is used as a variable for datatypes, but isnβt declared to be a variable for such in definition 2.1.5.
We may freely assume standard function symbols, such as 0, 1, +, β, and pairing (-, -), with their usual meanings and types
[β¦]
We may freely assume standard predicate symbols, such as =, <, β€, tupling
(-, . . . , -) and projections ππ , with their usual meanings. Meaning will always be
clear.
Tupling and projections are functions, not (generally) predicates. Itβs not clear to me what they should mean if we tried interpreting them as predicates.
Unless otherwise stated, we will follow a convention that variable symbols named π and π (like π, πβ², π1, πβ²β², and so on) will have a datatype, and variable symbols of the form π may have any datatype.
Iβm not really sure what this is trying to say. Is it stating that as and bs will always have a fixed datatype given by the context in which they are used, while c will never have such? I also didnβt see anywhere in the paper where c was used as a variable (except for thresholds), so this aside doesnβt seem needed.
f β FSymb to each of which is associated a type type(f) of the form πΎ β πΎ
What is βββ, and where is it? Itβs actually used in quite a few places. Obviously, I know itβs a function type, but thatβs not declared anywhere, and its semantics is never described. What is βtypeβ; the function youβre applying to f
?
an interpretation function π (P) : Time β Place β πΎ β Bool
[β¦]
A function π (msg) : (N Γ Place Γ Place Γ Data) β Bool.
why is one curried and the other not? Also, some clarification/intuition on why the signature of π (msg) looks like that would be good.
- πβπ is the model obtained by restricting π to times up to and including π.
- πβπ is the model obtained by restricting π to times from π onwards.
Does βfrom π onwardsβ include π?
Also, there should be some kind of formal restriction of Time (e.g. that itβs linearly ordered) so that this can always be made sense of. As it stands, you have the naturals as an archetypal example of Time, but the semantics of π just says itβs an arbitrary set.
[[{π | π}]]π,π,π = {π β πΌ | π, π β¨π π [π:=π]}
Where does πΌ come from?
([[π‘]]π,π,π β Nβ₯#Time)/π, π β¨π @π‘ π
This is the middle-right formula of Figure 3. Where does π come from? If it is free/fresh, etc, that should be stated.
but none of the examples I was given have this form
What a bizarre line to read in a paper. Who gave them to you, and why is that sufficient for dismissal?
π΅ = {π β πΌ | π, π β¨π π [π:=π]} π΄ = {π β π΅ | π, π β¨π π [π:=π]} #π΄/#π΅ β₯ π π, π β¨π Ξ π π : π.π
First formula in figure 3
[β¦]
π΅ = {π β πΌ | π, π β¨π π [π:=π]} and π΄ = {π β πΌ | π, π β¨π π [π:=π] β§ π [π:=π]}
in remark 2.3.1. Is that first A supposed to be a subset of B? Is that second A meant not to be a subset of B? If both are correct and equivalent, should the notations be made consistent?
Threshold. To express Ξ ππ π.π using Ξ π π.π , we just write [β¦]
What is n in that formula? Presumably c?
Future work could explore could explore information flow control
Typo.
but usually that a reasonable first approximation to real life
Typo.
β¦
I think the paper would be improved with some better intuition early on. For example, it doesnβt seem like intuitive, straightforward explanations of @_π‘ π, in_π(π‘), or out_π(π‘) are ever made.