Lambda the Ultimate

... especially when they're ambiguous. Last time "I.F." showed up on LtU, it meant "interactive fiction". This time, it took a couple of clicks to locate the expansion as "Independence-Friendly". Thanks for the link, Andris.

Understanding why it works for you might help me work this out for myself.

I didn't put it into good use yet, but I have some ideas. Prepare for a brain dump.

On my day job I worked for several years on BPM and similar topics, and the state of the art amazed me (and not because of its great achievements). Abundance of standards for definition of business processes, orchestrations, and choreography is probably even more pronounced than in other parts of IT industry. I tried to use some formalism instead of standard, and found that pi and join calculi are far from satisfying requirements. As strange as it may sound I needed types, even more - I needed contracts or protocols. I played with linear logic a bit (Curry-Howard to the rescue). It seemed almost the right thing. Then I stumbled upon computational logic (CL). At about the same time I got interested with the notion of computability, Turing machines of all sorts, Gödel's theorems, ..., so CL looked very interesting. Another attractive property of CL was its approach of starting from semantic (unlike linear logic). I had some sentiments about CL not covering multiplayer games, as that would be handy in business cases.

Having said that, I plan to try and extend the ideas from OP paper a bit (as far as non-academic can :) ). One thing is reflection and interpretation (particularly reflective towers) - how can it be described by game semantics? Who are the players?
Another thing is not of practical interest for me, but more of a hobby (though it might help me to understand distributed computing) - what constraints on the structure of the game make it compatible with relativistic physics, thus yielding the notion of relativistic computability?
The last thing is quite minor, but looks useful for practice: I consider to replace permutation of roles by a function (probably not even injective) of role mapping for purpose of modularity and reuse. The question is, how this would affect the properties of the logic?
[on edit: almost forgot about this important feature - cancellation and "garbage collection" of cancelled (irrelevant) moves]

As you can see, my interest, while avid, is based on very raw ideas.
Hope some of them might be interesting to somebody else.

PS: I speculate that at least couple of LtU readers might find the OP ideas useful for game development :)

I suspect, but am not competent to prove, that this is related to Modal Logics, particularly those discussed in Reasoning About Knowledge. If so, there are several potential application domains, e.g. economics and distributed systems generally. I'm also reminded of the two-envelope problem, about which these authors say "We conclude that the two-envelope problem does not allow a satisfactory solution," which seems to me to be addressed by Pollock in Thinking about Acting: Logical Foundations for Rational Decision Making, where he notes:

In chapter eight, it is argued first that actions cannot be evaluated in terms of their expected values as ordinarily defined, because that does not take account of the fact that a cognizer may be unable to perform an action, and may even be unable to try to perform it. An alternative notion of "expected utility" is defined to be used in place of expected values. In chapter nine it is argued that individual actions cannot be the proper objects of decision-theoretic evaluation. We must instead choose plans, and select actions indirectly on the grounds that they are prescribed by the plans we adopt. However, our objective cannot be to find plans with maximal expected utilities. Plans cannot be meaningfully compared in that way.

Of course, it's worth noting the last comment in the paper above:

The logic and semantics we have developed appears to flow from very natural intuitions.
These should be supported by a range of convincing examples and applications.

Yes. Yes, they should.

Way of topic: reading the title, I guess it should have been posted to the Community Enforcement Discussion thread.

Me too...

Is it criticism of the title, or of its appearance on the front page?

Do you suggest I change the title of the paper? :)

Just in case somebody have responded without reading at least the first page of the paper - it IS about logic, game semantics, and concurrency. And some category theory is used, as well.
It just happens to have a bit too frivolous title.

No, no. It just tells you something about the state LtU at the moment, that the title was a bit confusing.