Research Interests
I work with programming languages and their type systems. Specifically, the design and implementation of dependent type systems and their applications in the univalent foundations of mathematics. My choice of programming languages are Rust, Arend (developer), Agda (contributor), Perl, Kotlin and Haskell.
Apart from that, I am also interested in the design and implementation of Integrated Development Environments (aka IDEs) and their plugins.
Activities
- Intern at JetBrains, remote, Spring 2020 - Present (Project Arend).
- Participate the Penn State MC REU program, State College, PA, Summer 2019.
- Intern at PingCAP, remote, Summer 2018 - Summer 2019.
- Intern at Sourcebrella, Shenzhen, China, Spring 2018 - Summer 2018.
- Open-source contributions.
Toys
Toy programming languages implemented by me (> 80% contribution), all dependently-typed.
- Mini-TT, minimal DT language, reimplemented in Rust.
- Voile, with non-dependent version of row-polymorphism.
- Narc (WIP), with Agda-style dependent pattern matching.
Some interesting tools:
- agda-tac, an external tactic framework for the Agda programming language.
- intellij-dtlc, an IntelliJ IDEA plugin with most code generated, that supports > 10 languages.
- intellij-pest, IntelliJ IDEA plugin for a grammar language with live parsing preview.
- vscode-arend VSCode extension for the Arend proof assistant.
- arend-language-server Language Server Protocol implementation for the Arend proof assistant.
- arend-io Arend library that implements strings, IO and
unsafePerformIO.
The best way to understand type theory is to implement it!
– Anders Mörtberg