Mikołaj Bojańczyk, Laurent Braud, Bartek Klin, Slawomir Lasota
Towards nominal computation. POPL, 2012 PDF
Mikołaj Bojańczyk, Szymon Torunczyk
Imperative Programming in Sets with Atoms. FSTTCS, 2012 PDF
Mikołaj Bojańczyk, Thomas Place
Toward Model Theory with Data Values. ICALP (2), 2012 PDF
Modelling Infinite Structures with Atoms. WoLLIC, 2013 PDF
Mikołaj Bojańczyk, Bartek Klin, Slawomir Lasota, 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. I am very slowly writing a book on this, although progress has recently stalled. 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.
We began by studying orbit-finite automata and monoids, but we have subsequently moved on to a study of general computation, including a functional programming language in paper , an imperative programming language in paper , and a study of Turing machines . Some highlights: there is a robust notion of computation for orbit-finite sets, with algorithms that can (and are) implemented on actual computers, although paper  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 [3,4] study logic in sets with atoms. Paper  shows that orbit-finite Boolean operations can be eliminated. Paper  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 . 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.