A simpler encoding of indexed types. - Tesla Zhang (CoRR, 2021)

Elegant elaboration with function invocation. - Tesla Zhang (CoRR, 2021)

Type theories in category theory. - Tesla Zhang (CoRR, 2021)

A tutorial on implementing De Morgan cubical type theory. - Tesla Zhang (CoRR, 2022)

Two tricks to trivialize higher-indexed families. - Tesla Zhang (CoRR, 2023)

Three non-cubical applications of extension types. - Tesla Zhang (CoRR, 2023)

(Co)condition hits the Path. - Tesla Zhang; Valery Isaev (CoRR, 2024)

A Language-Agnostic Logical Relation for Message-Passing Protocols. - Tesla Zhang; Sonya Simkin; Rui Li; Yue Yao; Stephanie Balzer (CoRR, 2025)