1. Mikołaj Bojańczyk
   Nominal Monoids. Theory Comput. Syst., 2013   PDF

2. Mikołaj Bojańczyk, Bartek Klin, Slawomir Lasota 0001
   Automata theory in nominal sets. Log. Methods Comput. Sci., 2014   PDF

3. Mikołaj Bojańczyk, Slawomir Lasota 0001
   A Machine-Independent Characterization of Timed Languages. ICALP (2), 2012   PDF

4. Mikołaj Bojańczyk, Laurent Braud, Bartek Klin, Slawomir Lasota 0001
   Towards nominal computation. POPL, 2012   PDF

5. Mikołaj Bojańczyk, Szymon Torunczyk
   Imperative Programming in Sets with Atoms. FSTTCS, 2012   PDF

6. Mikołaj Bojańczyk, Thomas Place
   Toward Model Theory with Data Values. ICALP (2), 2012   PDF

7. Mikołaj Bojańczyk, Luc Segoufin, Szymon Torunczyk
   Verification of database-driven systems via amalgamation. PODS, 2013   PDF

8. Mikołaj Bojańczyk
   Modelling Infinite Structures with Atoms. WoLLIC, 2013   PDF

9. Mikołaj Bojańczyk, Bartek Klin, Slawomir Lasota 0001, Szymon Torunczyk
   Turing Machines with Atoms. LICS, 2013   PDF

Atoms are a theory project that we are developing in Warsaw, which even has its blog and a book. The project was originally motivated by trying to understand automata on data words and data trees. The idea is to consider sets with ur-elements that are called atoms, and to consider a different notion of finiteness: a set is called orbit-finite if it has finitely many elements up to permutations of the atoms.

Automata and monoids

We began by studying orbit-finite automata and monoids. The papers [1,2,3,7] are on the question: “what is a regular language in sets with atoms?”. Paper [1] is about orbit-finite monoids, and it proves a Schützenberger theorem for them, demonstrating that the structural theory of monoids extends rather smoothly to orbit-finite monoids. Paper [1] is a journal version of

Mikołaj Bojańczyk
Data Monoids. STACS, 2011   PDF

In the STACS paper above, the terminology is a bit antiquated, because at the time I was not aware of the existence of nominal sets or atoms. Paper [2] studies orbit-finite automata, which are more powerful than finite monoids. In a certain sense, orbit-finite automata are the same thing as register automata of Francez and Kaminski, but the formalism of orbit-finiteness is a bit more flexible, e.g. allowing a Myhill-Nerode theorem and effective minimization. Paper [2] is a journal version of

Mikołaj Bojańczyk, Bartek Klin, Slawomir Lasota 0001
Automata with Group Actions. LICS, 2011   PDF

which is already aware of nominal sets. I think that maybe an easier to follow description of the topic of [2] is the book mentioned above. Paper [3] continues the study of the Myhill-Nerode theorem, but it does so for a kind of atoms that correspond to timed automata, where the assumptions of paper [2] are not satisfied. Finally, paper [7] gives a database angle on the automata from [2], although it tries to avoid using the word atom in order not to annoy database theorists, including Luc Segoufin.

 

More powerful computation models

After studying automata and monoids, we have subsequently moved on to a study of general computation, including a functional programming language in paper [4], an imperative programming language in paper [5], and a study of Turing machines [9]. Some highlights: there is a robust notion of computation for orbit-finite sets, with algorithms that can be (and are implemented, both functional and imperative) implemented on actual computers, although paper [9] shows that Turing machines are not the correct model (e.g. they do not determinize, although proving this requires use of the Cai-Fürer-Immermann construction).

Papers [6,8] study logic in sets with atoms. Paper [6] shows that orbit-finite Boolean operations can be eliminated.  Paper [8] asks if there is a fundamental conflict between the finite support condition that underlies sets with atoms, and the need to study infinite objects.

Attention: there is a bug in the proof of paper [6]. Namely, Theorem 6.2 is false, a counterexample being obtained using the same CFI-inspired construction as in Theorem III.1 here.  However, Tomek Gogacz has proposed in oral communication a modification of Theorem 6.2, which allows one to recover the main Theorem 3.5.