@inproceedings{chen_etal_2026, series={CPP ’26}, title={Can We Formalise Type Theory Intrinsically without Any Compromise? A Case Study in Cubical Agda}, url={http://dx.doi.org/10.1145/3779031.3779090}, DOI={10.1145/3779031.3779090}, booktitle={Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs}, publisher={ACM}, author={Chen, Liang-Ting and Nordvall Forsberg, Fredrik and Tsai, Tzu-Chun}, year={2026}, month=jan, pages={201–215}, collection={CPP ’26} }