Typed Abstract Syntax
Julianna Zsidó · 2010
In order to specify the behavior of programming languages, to investigate their properties and to allow certification of their implementations, one studies formal models of existing programming languages. This study splits into the study of syntax and semantics, where the latter is based on appropriate formal models for the syntax. This PhD thesis is located in the syntactic part and is mainly concerned with two approaches to abstract syntax with variable binding. Both make use of the language of category theory. The first one is in the spirit of the category theoretic approach to algebraic theories. The second one is based on the notion of monads and introduces modules on monads instead of working with functors and their algebras. Furthermore the latter approach is adapted to a larger class of typed syntax with types depending on terms.