Time and Location

  • Date: Thursday, August 6
  • Time: 3:00-4:00 PM
  • Location: Luddy Hall (BLIF) 1104
  • Host: Prof. Carlo Angiuli, Computer Science

Abstract

XTT, which is a cubical reconstruction of observational type theory designed to combine extensional equality principles with a computational interpretation, is known to satisfy closed Boolean canonicity. A normalization theorem for univalent Cartesian cubical type theory yields decidability of judgmental equality. Still, it remains unclear whether the result can be extended to XTT. We make partial progress on this question by introducing XTT-minus, a universe-free cubical fragment of XTT with booleans, dependent products and sums, proof-irrelevant dependent paths, regular coercion, and homogeneous composition over arbitrary finite systems. In this talk, we prove that judgmental conversion for XTT-minus is decidable for open terms in arbitrary finite dimension and face contexts. A complete Agda formalization is in progress.

(Jilin Wang is a PhD student at Zhejiang University.)