Leonhard Staut: Bachelor's Thesis
Nu-Trees 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 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.
Formalization
Presentations
-
Initial Seminar Talk:
Slides
(April 28th, 2017)
-
Second Seminar Talk:
Slides
(June 30th, 2017)
-
Third Seminar Talk:
Slides
(September 20th, 2017)
Legal notice, Privacy policy
