Tesla Zhang

JetBrains Research, RemoteJan, 2020 – Dec, 2020
HoTT and Dependent Types, Interactive Theorem Prover Development

• Used features like gradle composite build and buildSrc to reduce build time and improve automation.
• Improved the language/IDE, such as sections, hygiene macros, FinFin type with elaborative subtyping, semantic highlighting, etc.
• Created an extensible REPL engine, provided implementations in CLI (with contextual completion using jline3jline3) and in IntelliJ IDEA (interacts with the opened project, supports completion, highlighting and goto definition).
• Designed and implemented an expression type-checking debugger that supports step-into and displays local context and expressions as stack frames.

PLCT Lab, RemoteDec, 2020 – Present
Implementation of Dependent Types, Opensource Maintainer

• Leading a team to explore modern techniques in type theory implementation, such as pattern unification, elimination of dependent pattern matching, Cartesian cubical type theory, termination check of recursive functions, phase distinction between layers of a type theory, etc.
• Organized reading activities on design and implementation of type theory, presented several talks in ∞-Type Café Summer School on Type Theory (in Chinese).

RisingWave Labs, RemoteJul, 2022 – Jul, 2023
Streaming Database, Developer Intern

• Proposed an overhaul of the query plan AST design, which better facilitates the enum feature implemented in the Rust language.
• Implemented a pretty printing framework for trees with smart line fitting and Unicode art. Integrated into SQL explain.

Sourcebrella Inc., Shenzhen, ChinaFeb, 2018 – Jul, 2018
Static Analysis, Compiler Frontend, IDE Plugin Development

• Created IntelliJ/CLion/Eclipse plugin for the Pinpoint analyzer. Co-worked on the SonarQube plugin.
• Created a multi-threading cross Java/Kotlin source code indexer which can index Hadoop within 4 minutes.
• Learned a lot about Linux programming and the Clang/LLVM codebase.

PingCAP Inc., RemoteAug, 2018 – Aug, 2019
Distributed Storage Systems, TiKV Intern – Ecosystem Team

• Improved many TiKV-relevant libraries, like optimizing the performance of grpcio, adding new features to procinfo.
• Helped to migrate the Protocol-Buffer library used by TiKV and its Raft implementation.
• Learned a lot about Rust programming, distributed system, working remotely, and databases.

Aya Prover, Practical Implementation of Dependent Types (role: project leader) aya-prover/aya-dev

• Supports dependent types, dependent pattern matching with confluence check for overlapping clauses, higher inductive types, GADTs (paper published), hierarchial universes, cubical type theory features, and implicit arguments.
• Can export elaboration result to HTML or

  L

  . Can JIT-compile closures into JVM using HOAS, Can refine patterns using coverage information. Supports both LSP in VSCode and IntelliJ PSI. Provide jlink binary releases.

IntelliJ Pest, Pest language plugin for IntelliJ Platform pest-parser/intellij-pest

• Semantic-based highlighting, completion, navigation, definition extraction/inlining, and Rust plugin integration.
• Provides live preview – test grammar files by dynamically highlighting user code according to the grammar on the fly. These highlighted code could be exported to HTML.

Multi-Campus REU, State CollegeMay, 2019 – Aug, 2019

• Extensively studied the literature on row polymorphism and record calculus.
• Implemented ( owo-lang/voile-rs) and formalized a row polymorphic dependent type theory.