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

https://orcid.org/0000-0002-9050-846X

I have a blog, a GitHub profile, a bibliography, and an arXiv profile.

My resume has a simplified version and a full version. These are not for research – publications are included in the bibliography.

Research Interests

I work with programming languages, their type theories, and semantics. Specifically, the design and implementation of dependent type systems and their applications in the univalent foundations of mathematics. I want to improve type theories by developing useful types with good computational properties.

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.

I’m developing Aya, a practical proof assistant which features in generalization of definitional equalities and overlapping but confluent pattern matching. It also has some HoTT features similar to Arend.

Activities

• 2 talks (one roundtable discussion and one talk) in WITS22 on Aya language features.
• Intern team lead at PLCT Lab, remote, Spring 2021 (Project Aya).
• Intern at JetBrains Research, remote, 2020 (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 (now Ant Financial Code Insight), Shenzhen, China, Spring 2018 - Summer 2018.
• Open-source contributions.

Projects

• Type theory in category theory, lecture notes.
  • The type theory extracted from the lecture notes.

Toy programming languages implemented by me (> 80% contribution), all dependently-typed.

• Mini-TT, minimal DT language with NbE, reimplemented in Rust.
• Voile, with non-dependent version of row-polymorphism.
• Narc, an abandoned project which aims at reproducing Agda-style dependent pattern matching in an imperative language.

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