Viewing profile — mathetic

Sorry, I didn't mean to mislead. I was exemplifying ways of subtly leaking data. In the next paragraph, I clarify what we cover with the following: > Namely, we implement a type sy…

I used natural numbers as a simplification. In full generality, you can use a lattice where min and max are replaced by meet and join operations. Then you can have categories that …

The goal is the same but the approach is different. This is entirely compile time and it covers all executions of the program, whereas taint analysis done at runtime and consider o…

The language is just assignment to simple variables (like `=` in C), sequencing (like `;` in C), if-then-else statements, and while loops. The simple version uses algebraic data ty…

Let's say we have `a, b, d : 0` and `c : 999`. Then `a := b :>> c := d` according to your rule is well-typed and has a security level `999`. Now let's say I have a conditional expr…

My bad, sorry =) The share from this story is that we can enforce privacy just as we enforce more traditional types at no runtime cost. It scales because it is compositional and co…

That is a different notion of typing. The type systems you are referring to (which is how they are commonly understood) classify data according to the operations they support. In t…

Wouldn't that require the programmer to be adversarial? Since all type systems have escape hatches, I don't think they would be resilient at all in adversarial settings. This is mo…

The point is often you don't need to. If you use Google docs, the chances are you will be editing it disjointly most of the time and occasionally you'll edit the same bit of the do…

So I use QuickCheck often and I'm a true believer, but the point this post is making is absolutely justified. Tying the test generation to the type is often requires some creative …

That doesn't help at all because although Datalog is a syntactic fragment, its dynamic semantics are very different, so the operations defined in Prolog standard are suggestive at …

I think it's more cultural than anything else. SQL, despite being declarative itself, has a more imperative feel to it for some people (recursion being at the fringes of its standa…

OP here. Happy to answer any questions.

That's not always an option. Your career very much depends on consistently publishing in "A" venues (conference/journal). So it depends on your subcommunity's opinion on open acces…

It is a breath of fresh air seeing someone, after earning some success and wealth, still remembers the values he started out with. Going a step further and being a good leader woul…

Yes, I was thinking total with respect to _intuitive_ arguments, but wrote injective. Sorry.

Ah, that's a problem with many facets. It is not that we can't come up with a logic language that is more declarative, it is just that telling the program everything about the univ…

Sure. Which subjects are you interested in?

I'm a grad student and I spend a lot of my time reading CS papers. It is amazing that you want to start reading CS papers and I highly encourage it. However, if you don't have a CS…

We got caught up doing science of it all.

Nope. Strange loops are not by definition not intentionally circular (while a circular graph in a file system is in this case). He makes that clear I think in the final chapter of …