Leonhard Staut: Bachelor's Thesis
Nu-Trees in Coq: Their Language and Automata
Advisor: Dominik Kirst
Supervisor: Gert Smolka
We study tree languages obtained by systematically permuting names over an infinite alphabet.
For this purpose we define nu-trees which contain nu-nodes to bind names.
We use nominal sets embedded in type theory to formalize types with a permutation action and use this as a framework for our development.
The language of a nu-tree is a class of pure trees. We show that this class is decidable and
show equivalence laws for nu-tree languages which correspond to the nominal axioms proposed by Gabbay.
Furthermore we introduce an automaton model for nu-trees which follows the definition of dependency tree automata by Stirling.
We show that acceptance is decidable for our model.
Initial Seminar Talk:
(April 28th, 2017)
Second Seminar Talk:
(June 30th, 2017)
Third Seminar Talk:
(September 20th, 2017)