- This thesis is about inductive structures with alpha conversion
- Inductive structure =
- (Co)inductively defined sets
- Data types
- (Co)inductive "reasoning" over them
- Inductive structure examples: CFGs, datatypes, circuits, natural numbers, operational semantics, typing judgements
- Novel solution to the problem of abstract syntax with variable binding
- ?? R4.3
- Syntax = what we write it as, semantics = object in formal framework, denotation = entity in nature