用户: Ice1000

$$🥑\stackrel{🧊🧠}{\Rightarrow }🌰.$$

Carnegie Mellon 编程语言方向博士在读!

主要研究类型论、编程语言理论和范畴论, 对几何学和拓扑学有一定兴趣. 主导开发了 Aya 证明器: https://www.aya-prover.org

如果您有想要阅读的相关词条, 可以在讨论页面进行请求.

1HoTT 2023 笔记

Andrej Bauer 作为神秘嘉宾登场, 当众发布了 HoTT book first edition!

目录

	1 抽象模态用于合并类型论
	2 双层类型论中的余纤维性
	3 缩积操作的五边形公理
	4 综合代数几何
	5 神谕模态
	6 代数类型论
	7 光滑无穷小分析
	8 有向立方类型论

没写的部分大概会无限期鸽, 我自己都忘得差不多了.

关于代数类型论: 说实话这个我觉得看用户: 算，就使劲算/如何把你的类型论变成一个范畴更有意义.

2文章搬运

目录

	1 代数与 PL 与 PL 之恋
	2 PL 中的 logical relation

3杂项

目录

	1 编程语言术语翻译表
	2 Sylvester 问题
	3 悠悠球编排范畴

术语翻译

千里冰封 • 英文 Tesla Zhang