The following content has been provided by the University of Erlangen-Nürnberg.

Thank you. Thank you very much. It's a pleasure to be here. As you've heard, I'm from computer

science theory and background in type theory, concurrency theory, and I've always been fascinated

by applications of concurrency theory, particularly in engineering context. And here is an issue

that I came across quite early in my career research and it has fascinated me ever since.

It's an issue that arises in synchronous programming languages, the compilation of synchronous

programming languages and execution of synchronous programming languages, a question of semantics.

And it's, I would argue arguably, the single most subtle issue in synchronous programming.

Synchronous programming is about programming mellia automata as such, theoretically not

so terribly tricky, but if you compose mellia automata and you create cycles, you end up

in causality cycles that are not easy to resolve. And you need mathematical techniques that

are beyond the standard techniques that we normally teach students in computer science,

techniques from logic and concurrency theory, game theory that can help, or I propose, can

help to resolve the problem, to give an idea, to attack it.

So right into the heart of the matter, what is the issue? It's synchronous programming,

I said, it's high level programming of mellia machines. And the key mathematical problem

you have to solve in a concurrent situation is to solve fixed points, fixed point equations

of, and here is the alarm bell that should be ringing, fixed points of non-monotonic

functionals. Standard theory, computer science theory says fixed points exist uniquely if

you have monotonic functions and lattices, but here it's not monotonic, so fixed points

do not have to exist, they don't have to be unique.

Not surprisingly, if you look into the engineering literature and the development of the semantics

of synchronous programming, you see a profusion of different proposals of how to organize

the interaction of cyclically connected mellia machines to give more or less coherent compositional

scalable semantics. You have a confusion of different dialects of synchronous programming,

ways of solving these cycles, and this is, there's another unique setting in which we

could address these, and the proposal that I have, and this is something I came up a

couple of years ago, is to use game theoretic approach which is quite modern, it's very

old in mathematics and logic particularly, but it's fairly new to be used in computer

science to solve recursive situations, self-references, particularly in interactive situations. It

introduces polarity into the semantics and this is what you need to resolve the causality

between a system and its environment, so it's quite natural. It's surprising that it comes

so late actually in the development of theory, of computer science.

The proposal I'm going to take you through is a way to try to understand the existing

semantics from a common ground, the game theoretic point of view, and I will show you in the

course of those following slides how we can recover the semantics of Gérard Berry of

STL, or imperative synchronous programming, or the state chart proposal, the semantics

for state charts proposed by Puglian-Charlotte in the 90s, and a recent proposal, sequentially

constructive charts by von Hanks-Leden, how to recover them uniformly from a common perspective

through games. Of course, this gives a playground to develop even more solutions, but now in

a way so you can compare them, hopefully, systematically, study different interpretations

and justify them in a way. Here is the plan, the roadmap. We start with

a brief introduction to synchronous programming up front. Then I will show you how the reaction

between synchronous components ends up being a fixed point, why this fixed point is tricky,

and then come up with a proposal to treat this as a game. We will then study four different

ways of fixing the game, playing the game, giving four different semantics, two of which

are well known, actually three of which are quite well known, you will see, and then I'll

finally come to this new proposal that we are working on at the moment, which is just

to semantically underpin this proposal which is called sequentially constructiveness for

synchronous programming language, SRL. That is quite a recent proposal by von Hanks-Leden.