28. Juli – 02. August 2013, Dagstuhl-Seminar 13311

Duality in Computer Science


Mai Gehrke (University of Paris VII, FR)
Jean-Eric Pin (University of Paris VII, FR)
Victor Selivanov (A. P. Ershov Institute – Novosibirsk, RU)
Dieter Spreen (Universität Siegen, DE)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl Report, Volume 3, Issue 7 Dagstuhl Report
Dagstuhl's Impact: Dokumente verfügbar


This seminar concentrated on applications of duality in computation, semantics, and formal languages.

Duality and computation

Consider the area of exact real number computation. Real numbers are abstract infinite objects. Computing machines, on the other hand, can only transform finite objects. However, each real number is uniquely determined by the collection of rational open intervals that contain it, or a certain sub-collection thereof. Rational intervals can be finitely described as a pair of rationals. So, in order to compute with real numbers one has to compute with certain properties, i.e., one no longer works in the space of the reals but in the algebra generated by these properties. In doing so, the open intervals are considered as first-class objects and the concept of point is taken as a derived one. This is exactly the approach of pointless topology which tries to develop analytical concepts in a pointfree way, hereby using constructive logic.

Duality and semantics

In logic, dualities have been used for relating syntactic and semantic approaches. Stone's original result is in fact of this type as it shows that clopen subsets of Stone spaces provide complete semantics for classical propositional logic. This base case has been generalized in various directions. There is a general scheme underlying this work: given a logic, construct its Lindenbaum algebra which in these cases is a Boolean algebra with unary operators. Jonsson-Tarski duality relates such algebras to binary relational structures which in the modal case are just Kripke frames. In this setting, a wide spectrum of duality tools are available, e.g. for building finite models, for obtaining interpolation results, for deciding logical equivalence and other issues. For infinitary logics, Stone-type dualities have also played an important role starting with Scott's groundbreaking first model of the lambda-calculus which is a Stone space. Subsequently Abramsky, Zhang and Vickers developed a propositional program logic, the logic of finite observations. More recently work of Jung, Moshier, and others has evolved this link between infinitary and finitary logics in the setting of logics for computation much further.

Duality and formal languages

The connection between profinite words and Stone spaces was already discovered by Almeida, but Pippenger was the first to formulate it in terms of Stone duality. Gehrke, Pin and Grigorieff lately systematized and extensively developed this discovery which led to new research efforts in formal language theory. A final goal is a general theory of recognition.

The seminar brought together researchers from mathematics, logic and theoretical computer science that share an interest in the fields of computing with infinite data, semantics and formal languages, and/or the application of duality results. The researchers came from 12, mostly European, countries, but also from Argentina, Japan, Russia, South Africa, and the United States.

Some of the specific questions that were investigated in talks and discussions:

  • Explore the use of the link between finitary and infinitary Stone dualities in other settings than semantics;
  • Explore the link between complexity theory and semantics provided by the connection via duality theory;
  • Identify the relationship between game semantics and dual spaces;
  • Explore the link between the profinite semi-groups used in formal language theory and logics given by state-based transition systems or categorical models)
Summary text license
  Creative Commons BY 3.0 Unported license
  Mai Gehrke, Jean-Eric Pin, Victor Selivanov, and Dieter Spreen

Related Dagstuhl-Seminar


  • Data Structures / Algorithms / Complexity
  • Semantics / Formal Methods
  • Verification / Logic


  • Stone-Priestley duality
  • Point free topology
  • Infinite computations
  • Exact real number computation
  • Computability in analysis
  • Hierarchies
  • Reducibility
  • Topological complexity
  • Domain theory
  • Semantics
  • Recognizability
  • Profinite topology


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.