is sometimes somewhere around at National Research University of Information Technologies, Mechanics and Optics (NRU ITMO), Saint-Petersburg, Russia.

Interests (in the order of preference):

- logics, type theory and related systems,
- functional programming and program analysis,
- mathematics in general,
- security and operating systems.

If not stated otherwise, every link I post anywhere was carefully read by me (every bit of it) and considered useful. If there is a link, it’s worth clicking.

- See activity. It describes (not really, as for now) things I’m doing or did in a readable way. Fast overview:
- I teach “Functional Programming and Proof Checking” and “Operating Systems”.
- I lead “Type Theory for Vegetables” seminar.
- I do different things with dependent types. Some of these are published.
- I have a couple of ideas concerning type theory foundations, but being unable to verify their consistency (for now) I prove properties of well-known formal systems in Agda to get more intuition. See notes for some examples.

- @oxij twitter account — a lot of random stuff about math, functional programming and security.
- oxij at github — my public repositories.

This page in an hCard. It does not include e-mail, though. You can produce it yourself by adding “oxij@” to the beginning of the domain name of this page.