Most of my experience is in tooling for software engineers. I spent 7 years working on GoLand, the IDE for Go. So I know a thing or two about compiler frontends, static analysis, and the UX of code editors.
- On development of static analysis tools for string-embedded languages (paper, talk in Russian).
- Intro to the Go programming language (lecture, in Russian).
- Inside GoLand: How Go language support works (meetup talk, in Russian).
- Supporting Go generics in GoLand (episode of the Generic Talks podcast, in Russian).
During my (unfinished) PhD, I focused on dependently typed programming languages and theorem provers. I also spent a year at the JetBrains Research HoTT group, working on tooling for the Arend theorem prover. So I know a bit about formalized mathematics and can formalize a theorem or two.
- Programming Language Foundations in Arend - the PLFA book re-written in Arend (Part 1). Mentioned on the original PLFA website.
- Formalization of Van Kampen’s theorem in Arend (partial).
- Intro to the View pattern for custom pattern-matching rules in dependently typed languages (blog post, in Russian).