Concurrent program development and correctness: S2S game strategies and constructive dynamic logic

The author summarizes work done in two areas: games for concurrency and constructive dynamic logic for concurrency. Two questions are also addressed: (1) what can be concluded in a language like dynamic logic about machine behavior if one has only partial knowledge of machine states, such as the contents of a few registers and stacks; and (2) can these computations be made naturally in constructive logic by term extraction and therefore be implementable