Speaker：Anjie Dong (The Chinese University of Hong Kong, Shenzhen)

Time：2026-9-1 15:00

Location：Conference Room S102 at Experiment Building at Haiyun Campus

Abstract:

Dependent type theory is both a foundation for mathematics and a theory with intrinsic computational meaning. As a result, equality comes in more than one form: some equalities hold directly by computation, while others must be proved within the theory.
This talk uses the distinction between these forms of equality as a guiding theme. We will discuss how computation enters into type checking, and explore the relationships among normalization, canonicity, and extensionality.
If two objects have already been proved equal, why can we not simply treat them as computationally identical? Which mathematical facts should be built into computation itself?