Interactive theorem proving, (constructive) type theory, programming languages, computability theory, constructive mathematics.
