• (λx. λy. λz. y@x.z) psu yqz5714 edu
• (λx. λy. λz. y@z.x) com ice1000kotlin foxmail

Research Interests

I work with programming languages, their type systems and underlying type theories. Specifically, the design and implementation of dependent type systems and their applications in the univalent foundations of mathematics.

Apart from that, I am also interested in the design and implementation of Integrated Development Environments (aka IDEs) and their plugins.

My choice of programming languages are Rust, Arend (developer, also develop intellij-arend), Agda (contributor, also contribute cubical-lib), Perl, Kotlin, Java and Haskell.

Activities

• Intern at JetBrains Research, remote, Spring 2020 - Present (Project Arend).
  • Group of HoTT and Dependent Types
• Participate the Penn State MC REU program, State College, PA, Summer 2019.
  • Supervised by Danfeng Zhang
• Intern at PingCAP, remote, Summer 2018 - Summer 2019.
• Intern at Sourcebrella, Shenzhen, China, Spring 2018 - Summer 2018.
• Open-source contributions.

Links

• Blog
• Resume (simplified, full)
• GitHub
• CodeWars
• Crates.io

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 programming language 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