∞-type Café 暑期学校 2023

01 Jun 2023

∞-type Café 暑期学校 2023将会在2023年7月2日正式举行。这次活动偶然源于一个提议，是否可以举办一个关于类型论暑期活动？由于当下国内研究类型论的学者非常少，相关资料也寥寥无几。于是我们决定尝试一下！

什么是类型论？它生于逻辑，长于数学，开花于计算机科学，结果于程序语言。它横跨了几个学科，彼此紧密。它在数学中作为新的数学基础出现，与集合论和范畴论并称。在计算机科学中，当提到类型的时候，我们会在第一时间想到各种编程语言，它可以帮助编译器或者解释器实现编译期的检查。柯里霍华德同构的出现使得我们重新开始审视类型，在命题即类型的观点下诞生了基于类型的交互式证明助手。把某个具体问题的证明当做程序来写成了现实，但是想要写出这样的程序，首先需要接受并熟悉它所对应的语言。在这一点上，无论是数学系还是计算机科学的学生都面临种种的问题。数学系的同学可需要先迈过编程这个坎，而计算机科学的同学要理解其背后的数学基础也并不太容易。到最后你历尽千辛万苦终于写出了可以被证明助手通过的程序，你是否问过自己它真的是一个证明吗？其中定义的那些函数是否是 well-defined? 其中构造的 objects 是否合理？其中使用的某些技巧是否正确？这些问题会推着你逐渐往前走，越走越远…

在某一天一个初学者偶然了解到类型论并开始了摸索，那么他的学习路径一定是充满了曲折的，因为我们当初也是这样走过来的。借助这次活动希望能帮助到更多想要学类型论的同学或者想要了解类型的同学，反过来我们也能交到更多的朋友，这是就是我们的简单而单纯的愿景。

引用Infinity Type Café群主狗先生的一句话:

在寒冷的夜晚，两个孩子生起了篝火，越来越多迷路的孩子来到了火堆边。他们感到无比幸福。
天亮了，孩子们慢慢地找到了自己的路，于是一个个地远去了。但他们永远不会忘记那个曾经给予过他们温暖的篝火。

Thorsten Altenkirch 对类型论的一个简短介绍:

面向怎样的听众

想要了解类型论的同学;
想要学习并使用类型论的同学;
具有一定类型论基础，想要往前再走一步的同学;
熟悉类型论，并想和我们讨论过去，当下，未来的同学。

基础课程

考虑每一个听众可能对类型论有不同的了解程度，并且这也是第一次暑校活动，所以我们专门地邀请了七位讲师给大家来一次贴心”补课”。以下课程参考了学习类型论的常规路径和本次暑校中talks要求的前置知识，课程讲解顺序从上至下。

希望以下课程能在不同程度上帮助到每一位听众，并且我们鼓励听众提前学习。如果在此过程中碰到问题，可以将其先存起来，然后在相应课程开始之后，直接向讲师提问。

Don’t sweat the stuff you don’t understand immediately. Keep moving!

Alias Qli, λ 演算和简单类型入门讲义, slides, 习题答案
面皮, 依值类型入门讲义, notes, 习题答案
kang, 一点儿综合同伦论讲义
oCaU, Agda使用入门（请提前安装Agda, 预习讲义）
天生万物以养人, Coq和Lean入门介绍讲义, Coq安装
Trebor, 范畴论与范畴语义(简单类型语义)入门
无懈可击99, 同伦类型论(HoTT)入门
千里冰封, 立方类型论(Cubical)入门, 摘要, 讲义

你可以查看我们未完成的如何学习类型作为进一步学习的参考。

课程对应的日程表如下:

7月2日-7月12日课程安排:

日期	下午2点-4点	晚上8点-9点
7月2日	Alias Qli λ演算和简单类型入门 B站视频: 1 2 3 STLC 的入门 (第一节) STLC 的延伸 (第二节)	无
7月3日	面皮依值类型入门 (第一节和第二节) B站视频: 1 2 3 4 5	Alias Qli λ演算和简单类型入门 (习题答疑1)
7月4日	kang 一点儿综合同伦论 (第一节和第二节) B站视频: 1 2	面皮依值类型入门 (习题答疑1) 腾讯会议链接
7月5日	无	oCaU Agda使用入门 (第一节) 腾讯会议链接
7月6日	天生万物以养人 Coq和Lean入门介绍 (第一节和第二节) 腾讯会议链接	oCaU Agda使用入门 (第二节) 腾讯会议链接
7月7日	无懈可击99 同伦类型论(HoTT)入门 (第一节和第二节) 腾讯会议链接	oCaU Agda使用入门 (第三课) 腾讯会议链接
7月8日	无	无
7月9日	Trebor 范畴论与范畴语义腾讯会议链接范畴-函子-自然变换 (第一节)	无懈可击99 同伦类型论(HoTT)入门 (习题答疑1) 腾讯会议链接
7月10日	无懈可击99 同伦类型论(HoTT)入门 (第三节和第四节) 腾讯会议链接	oCaU Agda使用入门 (习题答疑2) 腾讯会议链接 Trebor 范畴论与范畴语义 (习题答疑1) 腾讯会议链接
7月11日	无懈可击99 同伦类型论(HoTT)入门 (第五节) 腾讯会议链接	kang 一点儿综合同伦论 (第三节和第四节) 腾讯会议链接
7月12日	Trebor 范畴论与范畴语义腾讯会议链接伴随-米田引理 (第二节)	无懈可击99 同伦类型论(HoTT)入门 (习题答疑2) 腾讯会议链接 Trebor 范畴论与范畴语义 (习题答疑2) 腾讯会议链接

7月13日-7月15日课程安排:

日期	晚上8点-10点
7月13日	千里冰封立方类型论(Cubical)入门 (第一节和第二节) 腾讯会议链接
7月14日	千里冰封立方类型论(Cubical)入门 (第三节和第四节) 腾讯会议链接
7月15日	千里冰封立方类型论(Cubical)入门 (习题答疑1) 腾讯会议链接

注: 是否有习题主要看讲师自己是否有相关的安排，并且习题答疑也包含了讨论和提问的环节。

夏末演讲会

7月13日-7月15日演讲安排: 时间段安排上与基础课程基本相同, 注意13日到15日，白天是演讲，晚上是课程。

日期	下午2点-4点	晚上8点-10点
7月13日	Trebor 范畴语义基础	无
7月14日	林子篆 WASI 与 component model，跨语言的资源共享问题	无
7月15日	oCaU Agda 佐恩引理	无
7月16日	Anqur 心灵鸡汤: 你能从依赖类型版 JS 中获得什么	游客账户0x0 手把手教你实现 MLTT
7月17日	Trebor 综合数学综述	子鱼 LLM自动定理证明的进展
7月18日		魔理沙 Partial eval, Staging, Compiler and NBE
7月19日		千里冰封不那么 cool 的 cooltt
7月20日	Trebor 有效意象：构造主义与可计算性的桥梁（又名：如何编译你的证明）	oCaU Agda综合哥德尔不完备
7月21日
7月22日	Trebor 数学基础多元主义	千里冰封实现类型论中的高级特性
7月23日
7月24日		Gestellmensch 集合论已死,类型论当立

oCaU,
- Agda 佐恩引理
  
  佐恩引理是经典数学中最基础的定理之一。然而，作为直觉主义数学的前沿之一，同伦类型论 (HoTT) 在经典领域的扩展并未获得太多研究关注。本讲旨在填补这一空白，我们在HoTT的框架下展示对佐恩引理这一经典定理的证明，并顺带介绍其中涉及到的Agda语法和HoTT基本概念。 (知乎入口).
  
  前置知识: Agda
  注: 看需求可以顺带讲其中涉及到的 Agda 的语法，HoTT 的基本概念。
- Agda综合哥德尔不完备
  
  这是对哥德尔不完备定理的超简短形式化。我们在HoTT中引入邱奇-图灵论题（公理），建立综合递归论环境，以此直达哥德尔不完备定理论证的核心，而无需涉及复杂的计算模型和编码细节。
  
  前置知识: Agda + 数理逻辑的基础知识。
子鱼, LLM自动定理证明的进展

大语言模型驱动的自动定理证明的最新方法和结果的科普。

前置知识: 几乎没有。
注: 跟类型论关系不大，可当做 appetizer 或者 dessert。
Trebor,
- 范畴语义基础
  
  依值类型论是丛的语言。以此为主线，由浅入深讲解范畴语义的大框架，并且介绍范畴语义如何实际用于解决问题。
  
  前置知识: 熟悉依值类型论与范畴论基础。
  注: 可以分多次（越多次讲得越深，前置知识越少）。
- 综合数学综述
  
  我们习惯将每种数学对象都由更基本的数学对象表示：用Cauchy列编码实数，再用实数构造平面，进而研究平面几何。但是Euclid在《几何原本》中则是直接使用公理刻画想要研究的对象，从而构建了一个极其方便的研究几何的语言，正如编程语言中的DSL一样。本讲讲述一些综合数学的实例与应用。 nlab入口
  
  前置知识: 熟悉依值类型论与范畴论基础。
  注: 几个题目可以选一个讲，有时间可以都讲。
- 有效意象：构造主义与可计算性的桥梁（又名：如何编译你的证明）
  
  构造主义经常与可计算数学混同起来，然而许多构造主义的系统并没有显然的计算解释。另一方面，通常的可计算性仅仅处理了自然数之间的映射，而数学中常常需要处理其他事物的可计算性。有效意象给出了一套系统的链接构造主义与可计算性的语言。
  
  前置知识: 无需前置，少许逻辑和范畴的基本定义（如什么是全称命题，范畴的定义等）为佳。
  注: 几个题目可以选一个讲，有时间可以都讲。
- 数学基础多元主义
  
  注: 科普性质。
千里冰封 (全部讲座的摘要),
- 不那么 cool 的 cooltt
  
  Lamett 项目介绍，根据群友的意愿讲讲其中的组件。
  
  前置知识: 熟悉 MLTT 的实现(可以参考 Mini-TT 和 elaboration-zoo). 若想要理解其中的代码, 那就还需要基本的 Java 编程。
  注: 如果想听别的也可以直接联系我。
- 实现类型论中的高级特性
  
  简要介绍 elaboration-zoo 中介绍的几个高级的例子 (变量求解, 隐式参数等), 如何实现模式匹配。
  
  前置知识: 对这些被实现的功能本身有充分的理解。
  幻灯片
Gestellmensch, 集合论已死,类型论当立

HoTT,泛等公理的数学背景: 同伦论,模空间,还有很多相关的话题。以及为什么(同论)类型论是更好的数学基础。

前置知识: 不知道, 可能更多讲很泛泛的东西, 图一乐。
Anqur, 心灵鸡汤: 你能从依赖类型版 JS 中获得什么

RowScript 项目介绍; 如何从最基础 NbE 扩展语言功能; 讲点心灵鸡汤。

前置知识: 有依赖类型的直觉最好, 没有也没关系。
林子篆, WASI 与 component model，跨语言的资源共享问题

WASI 是让 WebAssembly 的程序可以操作系统资源而设计的接口，component model 让不同语言实现的模块可以交换资料。如何用 linear type 与 effect system 避免模块见资源交换的错误，实际上又有什么限制呢？

前置知识: 大概知道不可变的 functional programming 就好了
注:
- 在此介绍的方法不一定能进入标准，标准组织中有人有兴趣但是
- 不会用正式跟数学化的方法介绍，这些模型都是原型，在更确定会进入标准之前我不会进行更深入的检查
魔理沙, Partial eval, Staging, Compiler and NBE

介绍partial evaluator，并且以这个为基准，引入跟staging, compiler, normalization by evaluation等技术的联系。

前置知识: 最好懂definitional interpreter。
游客账户0x0, 手把手教你实现 MLTT

在ocaml中实现Per Martin-Löf type theory。

热烈欢迎各路老师和同学来分享topics!

目前听众希望的talks

类型论的学习路线图 (希望演讲人讲述下自己类型论的学习过程。最好对每段学习过程讲下：难点以及怎么度过难点，推荐学习书籍论文等。)
Cubical Agda 的钉子 (请介绍不需要太多前置的好做的漂亮的小众领域。例：https://arxiv.org/pdf/2208.03844.pdf#page22)
类型论的设计哲学：如何判断不同设计的好坏？
从数学哲学或数理逻辑视角对同伦类型论作为数学基础的介绍
类型论的入门知识（零基础适用）
如何用代码实现类型系统（零基础）
范畴语义 (对于 ATP 算法设计; MLTT 和 Cubical 的)
HoTT 的进阶 (希望可以讲一些 high level 的东西和比较直观的东西，比如 HoTT 的发展或者构建过程，为什么要引入 homotopy theory, 带了一些什么好的结果等等)
Cubical 的入门
类型论的应用 (如《类型论简史》展望部分所提的问题, 以及严肃地考虑类型论在工业界的应用)
类型系统的（高效）实现 (比如 MLTT type check 的实现)
综合数学
同伦类型论以及如何应用到数学里
同伦类型论和 ZFC 比较优点在哪
类型论在计算机安全中的应用 (例如区块链和软件安全等)
mathlib 的项目实践

热烈各位观众朋友来分享想要听的 topics!

∞-type Café Summer School TuT

∞-type Café 暑期学校 2023

相关重要信息

面向怎样的听众

基础课程

夏末演讲会

目前听众希望的talks

相关问题

相关人员

讲师

特别演讲人

组织者