Leonhard Staut: Bachelor's Thesis
NuTrees in Coq: Their Language and Automata
Advisor: Dominik Kirst
Supervisor: Gert Smolka
Abstract
We study tree languages obtained by systematically permuting names over an infinite alphabet.
For this purpose we define nutrees which contain nunodes 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 nutree is a class of pure trees. We show that this class is decidable and
show equivalence laws for nutree languages which correspond to the nominal axioms proposed by Gabbay.
Furthermore we introduce an automaton model for nutrees which follows the definition of dependency tree automata by Stirling.
We show that acceptance is decidable for our model.
Formalization
Presentations

Initial Seminar Talk:
Slides
(April 28th, 2017)

Second Seminar Talk:
Slides
(June 30th, 2017)

Third Seminar Talk:
Slides
(September 20th, 2017)
Leonhard Staut,
Mon Oct 2 16:13:47 2017