Author: Markus Michelbrink
Title: Interfaces as games, programs as strategies
Abstract: 
Peter Hancock and Anton Setzer developed the notion of
interface to introduce interactive programming into dependent type
theory. We generalise their notion and get an even simpler definition
for interfaces. With this definition the relationship of interfaces to
games becomes apparent. In fact from a game theoretical point of view
interfaces are nothing than special games. Programs are strategies for
these games. There is an obvious notion of refinement which coincides
exactly with thpe intuition o f what a refinement should do. Interfaces
together with the refinement relation build a complete lattice
(without least and greatest element) in the sense that every family of
interfaces has a least common refinement and there is an interface
such that all members of this family refine this interface and this
interface is a refinement for every other interface with this
property. A program/strategy on a refinement of an interface gives a
strategy on the interface.  We can define several operators on
interfaces: tensor, par, choice, bang et cetera. Every notion has a
dual notion by interchanging the viewpoint of player and
opponent. Lollipop is defined as usual in terms of tensor and
negation. We define the notion of fair strategy on $A \multimap B$. A
fair strategy is essentially a pair of a strategy and a proof that
this strategy plays in both games eventually. By a slight restriction
of the notion of interface we are able to define a composition for
fair strategies on $A \multimap B$ and $B \multimap C$. The obtained
strategy is again fair. We can define fair strategies on $A \multimap
A$ and $A \otimes (A \multimap B) \multimap B$. These strategies are
versions of copy-cat strategies. Identifying strategies by some kind
of behavioural equivalence we expect to receive a linear
category. However we have not checked all details until now. All
results so far can be achieved in intensional Martin-Loef Type Theory
and are verified in the t heorem prover Agda. There are numerous links
to other areas including refinement calculus, linear logic, game
semantics, formal topology, process algebra, model checking and so
on. However we have not explored all these relationships until now but
intend to do so in the future.