Leonhard Staut: Bachelor's Thesis

Saarland University Computer Science

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


Legal notice, Privacy policy