TOP
Suche auf der Schloss Dagstuhl Webseite
Sie suchen nach Informationen auf den Webseiten der einzelnen Seminare? - Dann:
Nicht fündig geworden? - Einige unserer Dienste laufen auf separaten Webseiten mit jeweils eigener Suche. Bitte beachten Sie folgende Liste:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminare
Innerhalb dieser Seite:
Externe Seiten:
  • DOOR (zum Registrieren eines Dagstuhl Aufenthaltes)
  • DOSA (zum Beantragen künftiger Dagstuhl Seminare oder Dagstuhl Perspektiven Workshops)
Publishing
Innerhalb dieser Seite:
Externe Seiten:
dblp
Innerhalb dieser Seite:
Externe Seiten:
  • die Informatik-Bibliographiedatenbank dblp


Dagstuhl-Seminar 13422

Nominal Computation Theory

( 13. Oct – 16. Oct, 2013 )

(zum Vergrößern in der Bildmitte klicken)

Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite: https://www.dagstuhl.de/13422

Organisatoren

Kontakt


Programm

Motivation

The underlying theme of this seminar is nominal sets, also known as sets with atoms, or Fraenkel-Mostowski sets, or permutation models. The seminar arises from a recent exciting and unexpected confluence of the following three distinct research directions.

  • Automata over infinite alphabets with applications to querying XML and databases.
  • Program semantics using nominal sets, with many applications to the syntax and semantics of programming language constructs that involve binding, or localising names.
  • Nominal calculi of concurrent processes (π-calculus, etc.), with applications to the automatic verification of process specifications.

The aim of the seminar is to profit from the excitement created by this confluence and to explore new directions with a new mix of research communities from computer science and mathematical logic. The central notion that underlies these new research directions is that of an orbit-finite set, a generalization and relaxation of the classical notion of finite set.

Such sets, although infinite, can be effectively represented and manipulated. For instance, alphabets and state spaces of register automata for data words, as well as values computed by programs that operate on nominal sets, are typically orbit-finite. This admits an effective realization of nominal computation.

The following gives a sample list of topics that will be of interest:

orbit-finite automata; computation theory in categories other than Set; applications to program verification; symmetry in domain theory; programming with orbit-finite sets; and computational complexity in the orbit-finite setting.


Summary

The short Dagstuhl seminar 13422 ``Nominal Computation Theory'' took place from October 13th to 16th, 2013. The topic of the seminar was the theory of nominal sets and their applications to Computer Science. The seminar arose from a recent exciting and unexpected confluence of the following three distinct research directions.

  • The research in automata theory on automata over infinite alphabets with applications to querying XML and databases.
  • The research in program semantics on nominal sets, with many applications to the syntax and semantics of programming language constructs that involve binding, or localising names.
  • The research in concurrency on nominal calculi ($pi$-calculus, etc) with applications to the automatic verification of process specifications.

In each of these three topics, an important role is played by name (or atom) symmetries and permutations, albeit for a priori different reasons. In the first case they arise from the way automata use registers to store letters, in the second case they are used to define the notion freshness, in the third case they are needed to minimize automata. In all three cases there is a connection with mathematical model theory, which is aimed at studying classes of mathematical structures definable by logical theories. The permutations allowed on atomic names can be usefully understood as automorphisms of a relational structure on those names. Model-theoretic notions such as homogeneity, algebraic closure and oligomorphic groups turn out very useful in describing those relational structures on atoms that yield meaningful theories of nominal sets.

The aim of the seminar was to profit from the excitement created by the confluence described above and to explore new directions with a new mix of research communities from computer science and mathematical logic. The main topics of interest included: automata and complexity theory in nominal sets, verification of nominal automata, symmetry in domain theory,and nominal programming.

The seminar was attended by 30 participants from 8 countries; 19 of them gave presentations, whose abstracts are included in this document. Four of the presentations (A. Pitts, M. Bojanczyk, B. Klin and N. Tzevelekos) were extended tutorials that presented various points of view on the background topics of the meeting. Other speakers presented the current state of the art in the field, with topic varying from mathematical insights into the nature of nominal sets (A. Blass, D. Petrisan), to applications in automata theory (V. Ciancia, T. Colcombet, S. Lasota, T. Suzuki) and computation theory (A. Dawar, S. Torunczyk), semantics and domain theory (R. Crole, J. Gabbay, S. Loesch, A. Murawski), Petri nets (R. Lazic), logic programming (J. Cheney) and theorem proving (C. Urban).

Copyright Mikolaj Bojanczyk, Bartek Klin, Alexander Kurz, and Andrew M. Pitts

Teilnehmer
  • Andreas R. Blass (University of Michigan - Ann Arbor, US) [dblp]
  • Mikolaj Bojanczyk (University of Warsaw, PL) [dblp]
  • James Cheney (University of Edinburgh, GB) [dblp]
  • Vincenzo Ciancia (CNR - Pisa, IT) [dblp]
  • Thomas Colcombet (CNRS / University Paris-Diderot, FR) [dblp]
  • Roy L. Crole (University of Leicester, GB) [dblp]
  • Anuj Dawar (University of Cambridge, GB) [dblp]
  • Murdoch Jamie Gabbay (Heriot-Watt University Edinburgh, GB) [dblp]
  • Fabio Gadducci (University of Pisa, IT) [dblp]
  • Tomasz Gogacz (University of Wroclaw, PL) [dblp]
  • Bartek Klin (University of Warsaw, PL) [dblp]
  • Alexander Kurz (University of Leicester, GB) [dblp]
  • Slawomir Lasota (University of Warsaw, PL) [dblp]
  • Ranko Lazic (University of Warwick - Coventry, GB) [dblp]
  • Steffen Lösch (University of Cambridge, GB) [dblp]
  • Justus Matthiesen (University of Cambridge, GB) [dblp]
  • Stefan Milius (Universität Erlangen-Nürnberg, DE) [dblp]
  • Ugo Montanari (University of Pisa, IT) [dblp]
  • Andrzej Murawski (University of Warwick - Coventry, GB) [dblp]
  • Joanna Ochremiak (University of Warsaw, PL) [dblp]
  • Daniela Petrisan (University of Leicester, GB) [dblp]
  • Andrew M. Pitts (University of Cambridge, GB) [dblp]
  • Luc Segoufin (ENS - Cachan, FR) [dblp]
  • Alexandra Silva (Radboud University Nijmegen, NL) [dblp]
  • Ian Stark (University of Edinburgh, GB) [dblp]
  • Tomoyuki Suzuki (Academy of Science - Prague, CZ) [dblp]
  • Szymon Torunczyk (University of Warsaw, PL) [dblp]
  • Emilio Tuosto (University of Leicester, GB) [dblp]
  • Nikos Tzevelekos (Queen Mary University of London, GB) [dblp]
  • Christian Urban (King's College London, GB) [dblp]

Klassifikation
  • programming languages / compiler
  • semantics / formal methods
  • verification / logic

Schlagworte
  • nominal sets
  • automata theory
  • HD-automata
  • orbit-finiteness