Cartesian Cubical Computational Type Theory
- 講者侯昆邦 博士 (University of Minnesota)
邀請人：穆信成 - 時間2018-07-24 (Tue.) 10:00 ~ 12:00
- 地點資訊所新館101演講廳
摘要
(Joint work with Carlo Angiuli, Evan Cavallo, Robert Harper, Jonathan Sterling and Todd Wilson)
Recent research revealed the deep connection between type theory and homotopy theory, which inspired a series of new type theories. The characteristic new features are univalence and higher inductive types, which have led to a fruitful development of synthetic homotopy theory. Unfortunately, those new features were originally introduced as axioms and disrupted the computational content of type theory, which affects their practicality in mechanizing proofs.
To date, the most promising approach to enjoy new features inspired by homotopy theory while retaining computational content is through cubical structure.
Cohen et al. constructed a type theory based on De Morgan cubes with both univalence and higher inductive types. Influenced by their work, we also built a type-theoretic semantics with all the features, but instead based on Cartesian cubes. In addition to using a different cubical structure, our semantics is built from computational content directly, following a computation-first methodology which itself is interesting.
In this talk, I will describe the computation-first methodology and how it can be extended to handle cubical structure.