Abstract

Sets with atoms, or nominal sets, offer a way to finitely present certain infinite data structures that exhibit enough symmetry. Essentially, such structures can be presented as their model-theoretic interpretations in a fixed infinite structure with a decidable first-order theory. Well-chosen programming language idioms can hide the interpretations from the programmer and let them work, most of the time, under the convenient intuition of looping and searching through infinite structures. I will say how, and give examples of when it does or does not work.

Video Recording