April 29th, 2013

beartato phd

(no subject)

That Martin Hoffmann paper I mentioned earlier is here:

In the back of my head I keep thinking about what it would mean to have these diamonds refer to permission-to-make-a-database-query or something like that. This would be a pretty big departure from the paper, since it has these tokens being consumed *and* generated (because they represent memory that can be reclaimed), and if you're keeping track of number of executions of some expensive piece of code, they'd just be consumed.
Collapse )
In fact, weirdly, as modal logic, ∃n.◇n ⊸ --- seems to behave like (Pfenning-style, not Awodey-Bauer-style) proof irrelevance! It's not transitive, because knowing that there's some cost to find out what the cost to complete a project is is not the same as knowing the cost to complete a project. This feels like some Fred Brooks shit right here.