Résumé | Nominal sets are a different kind of set theory, with a more relaxed notion of finiteness. They offer an elegant formalism for describing lambda-terms modulo alpha-conversion, or automata on data words. This presentation is an attempt at defining computation in nominal sets. We present a rudimentary programming language, called Nλ. The key idea is that it includes a native type for finite sets in the nominal sense. |