I am interested in Martin Löf’s type theory, dependent types, intuitionistic mathematics in general, category theory, and functional programming. I am particularly interested in the semantics of type theory in type theory, and the mathematical structures arising in programming languages and logics.

Functional Café

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!