Новости

версия для печати

Во вторник, 26 апреля 2005 года, в 15:40 в конференц-зале НМУ, Б. Власьевский, 11 состоится доклад «Games in computer science: a survey». Лектор – Pierre-Louis Curien (PPS, Universite Denis Diderot Paris, France).

In this talk, we shall survey different uses of games in computer science, which split roughly along issues of provability versus proofs. As for «provability», the satisfiability problem for various modal or temporal logics for reasoning on automata or concurrent systems is equivalent to the existence of winning strategies in associated games. It is also equivalent to the (non-)emptyness problem for languages recognized by various kinds of automata on (infinite) words or trees. In concurrency theory, the most studied notion of equivalence between processes is that of bisimulation, which can be also understood in terms of winning strategies.

As for «proofs», the emphasis is on the dynamics of strategies. Here, strategies are just another way of looking at proofs / programs / morphisms. Their composition corresponds to cut elimination / normalization. The subject of games semantics is very active since a decade, and has brought new results in the semantics of programming languages: simple and direct semantics for programming features such as control or references, full abstraction results connecting denotational and operational semantics tightly.

Московское Математическое Общество

Последние обновления