In this master's dissertation we examine intersection type systems that correspond to nominal automata. That is, for a given automaton we explain how to define a type system such that its programs are typable (in a certain sense) exactly if they evaluate to an input which is accepted by the automaton. This topic has its origins in software verification where automata are used to analyse properties of program executions. By defining an equivalent type system one obtains an associated type checking algorithm that solves the automaton acceptance problem elegantly and efficiently.
Much of the correspondence is independent from the actual automaton model, hence we factor out a fully generic treatment and evaluate its instantiation with several examples. Those include standard finitary automaton models on words and trees and nominal automaton models on words over atomic names and, lastly, trees with fresh name binding. The latter is what we call nu-trees and as the customised automaton model we introduce ranked nu-tree automata and discuss some of their properties.
The contributions of this work lie firstly in presenting type system-automaton correspondences independent from their original application in software verification. In particular, we provide self-contained introductions to intersection types, nominal sets and (nominal) automata theory. Moreover, by studying new concrete instances we strengthen the connection between the involved topics and encounter some actual synergetic effects.