Doctoral Speaking Skills Talk - Runming Li
October 28, 2026 12:00PM—1:00PM
Location:
6115
-
Gates and Hillman Centers
Speaker:
RUNMING LI,
Ph.D. Student, Computer Science Department, Carnegie Mellon University
https://www.cs.cmu.edu/~runmingl/
Intrinsically-typed presentations of type theory often use equality types in the meta-language to represent object-language judgmental equality. In such equational syntax, proof-relevant logical relations define computability predicates on judgmental equivalence classes of types and terms. This approach, however, does not directly account for reduction, which is directed and plays a central role in many logical-relations arguments.
This work develops a directed version of proof-relevant logical relations in simplicial homotopy type theory, a directed variant of homotopy type theory, where reductions are internalized as inequality types. We construct object syntax as a directed quotient inductive type. The central observation is that contravariant families in simplicial type theory provide exactly the proof-relevant form of closure under expansion for logical relations: computability evidence can be transported backward along reductions, with the required functoriality and universal property built in.
Using this observation, we construct a unary logical relations model with contravariant computability predicates and prove directed Boolean canonicity: every closed Boolean term reduces to either true or false. We then extend the construction to dependent types and universes, where a comonadic flat modality provides the discreteness needed for type conversion and universe predicates. Finally, we adapt the method to binary logical relations, separating vertical reduction from horizontal parametricity and obtaining a proof-relevant account of representation independence.
Presented as part of the PLunch Seminar Series
Presented in Partial Fulfillment of the CSD Speaking Skills Requirement
Contact
Matt Stewart