∞-type Café 暑期学校 2023将会在2023年7月2日正式举行。这次活动偶然源于一个提议，是否可以举办一个关于类型论暑期活动？ 由于当下国内研究类型论的学者非常少，相关资料也寥寥无几。于是我们决定尝试一下！
什么是类型论？ 它生于逻辑，长于数学，开花于计算机科学，结果于程序语言。它横跨了几个学科，彼此紧密。它在数学中作为新的数学基础出现，与集合论和范畴论并称。在计算机科学中，当提到类型的时候，我们会在第一时间想到各种编程语言，它可以帮助编译器或者解释器实现编译期的检查。柯里霍华德同构的出现使得我们重新开始审视类型，在命题即类型的观点下诞生了基于类型的交互式证明助手。把某个具体问题的证明当做程序来写成了现实，但是想要写出这样的程序，首先需要接受并熟悉它所对应的语言。在这一点上，无论是数学系还是计算机科学的学生都面临种种的问题。数学系的同学可需要先迈过编程这个坎，而计算机科学的同学要理解其背后的数学基础也并不太容易。到最后你历尽千辛万苦终于写出了可以被证明助手通过的程序，你是否问过自己它真的是一个证明吗？ 其中定义的那些函数是否是 well-defined? 其中构造的 objects 是否合理？ 其中使用的某些技巧是否正确？ 这些问题会推着你逐渐往前走，越走越远…
在某一天一个初学者偶然了解到类型论并开始了摸索，那么他的学习路径一定是充满了曲折的，因为我们当初也是这样走过来的。借助这次活动希望能帮助到更多想要学类型论的同学或者想要了解类型的同学，反过来我们也能交到更多的朋友，这是就是我们的简单而单纯的愿景。
引用Infinity Type Café群主狗先生的一句话:
在寒冷的夜晚，两个孩子生起了篝火，越来越多迷路的孩子来到了火堆边。他们感到无比幸福。
天亮了，孩子们慢慢地找到了自己的路，于是一个个地远去了。但他们永远不会忘记那个曾经给予过他们温暖的篝火。
Thorsten Altenkirch 对类型论的一个简短介绍:
相关重要信息
正式开始时间
: 2023年7月2日
课程时间段
: 每天的下午2-4点和晚上的8-10点
日历
:
Google Calendar
QQ群
: 791437680
Discord
:
join
Piazza课堂(提问和讨论的地方)
:
piazza
(上方QQ群和discord均可获取)
B站
:
无穷类型咖啡
Github
:
ntype-cafe-summer-school
面向观众的活动问卷
:
请务必填写
观众参与活动时间段问卷
：
问卷地址
面向怎样的听众
想要了解类型论的同学;
想要学习并使用类型论的同学;
具有一定类型论基础，想要往前再走一步的同学;
熟悉类型论，并想和我们讨论过去，当下，未来的同学。
考虑每一个听众可能对类型论有不同的了解程度，并且这也是第一次暑校活动，所以我们专门地邀请了七位讲师给大家来一次贴心”补课”。以下课程参考了学习类型论的常规路径和本次暑校中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日课程安排
:
7月10日
无懈可击99
同伦类型论(HoTT)入门 (第三节和第四节)
腾讯会议链接
oCaU
Agda使用入门 (习题答疑2)
腾讯会议链接
Trebor
范畴论与范畴语义 (习题答疑1)
腾讯会议链接
7月11日
无懈可击99
同伦类型论(HoTT)入门 (第五节)
腾讯会议链接
kang
一点儿综合同伦论 (第三节和第四节)
腾讯会议链接
7月12日
Trebor
范畴论与范畴语义
腾讯会议链接
伴随-米田引理 (第二节)
无懈可击99
同伦类型论(HoTT)入门 (习题答疑2)
腾讯会议链接
Trebor
范畴论与范畴语义 (习题答疑2)
腾讯会议链接
Agda 佐恩引理
佐恩引理是经典数学中最基础的定理之一。 然而，作为直觉主义数学的前沿之一，同伦类型论 (HoTT) 在经典领域的扩展并未获得太多研究关注。本讲旨在填补这一空白，我们在HoTT的框架下展示对佐恩引理这一经典定理的证明，并顺带介绍其中涉及到的Agda语法和HoTT基本概念。 (
知乎入口
).
前置知识: Agda
注: 看需求可以顺带讲其中涉及到的 Agda 的语法，HoTT 的基本概念。
Agda综合哥德尔不完备
这是对哥德尔不完备定理的超简短形式化。我们在HoTT中引入邱奇-图灵论题（公理），建立综合递归论环境，以此直达哥德尔不完备定理论证的核心，而无需涉及复杂的计算模型和编码细节。
前置知识: Agda + 数理逻辑的基础知识。
子鱼
,
LLM自动定理证明的进展
大语言模型驱动的自动定理证明的最新方法和结果的科普。
前置知识: 几乎没有。
注: 跟类型论关系不大，可当做 appetizer 或者 dessert。
Trebor
,
范畴语义基础
依值类型论是丛的语言。以此为主线，由浅入深讲解范畴语义的大框架，并且介绍范畴语义如何实际用于解决问题。
前置知识: 熟悉依值类型论与范畴论基础。
注: 可以分多次（越多次讲得越深，前置知识越少）。
综合数学综述
我们习惯将每种数学对象都由更基本的数学对象表示：用Cauchy列编码实数，再用实数构造平面，进而研究平面几何。但是Euclid在《几何原本》中则是直接使用公理刻画想要研究的对象，从而构建了一个极其方便的研究几何的语言，正如编程语言中的DSL一样。本讲讲述一些综合数学的实例与应用。
nlab入口
前置知识: 熟悉依值类型论与范畴论基础。
注: 几个题目可以选一个讲，有时间可以都讲。
有效意象：构造主义与可计算性的桥梁 （又名：如何编译你的证明）
构造主义经常与可计算数学混同起来，然而许多构造主义的系统并没有显然的计算解释。另一方面，通常的可计算性仅仅处理了自然数之间的映射，而数学中常常需要处理其他事物的可计算性。有效意象给出了一套系统的链接构造主义与可计算性的语言。
前置知识: 无需前置，少许逻辑和范畴的基本定义（如什么是全称命题，范畴的定义等）为佳。
注: 几个题目可以选一个讲，有时间可以都讲。
数学基础多元主义
注: 科普性质。
前置知识: 熟悉 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。
类型论的学习路线图
(希望演讲人讲述下自己类型论的学习过程。最好对每段学习过程讲下：难点以及怎么度过难点，推荐学习书籍论文等。)
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!
本次活动是线上还线下？
这次活动是否有录像？
B站会同步更新。
这次活动是否会提供课上内容的相关材料？
ntype-cafe-summer-school
会同步更新课上的讲义，幻灯片，代码和推荐课外内容。
人在国外有时差，如何参与这次活动？
我们目前考虑在中国时区的下午和晚上举行，请听众合理地安排一下时间。 如果时间上存在无法避免的冲突，可以参考Q2和Q3。
课后是否可以留一些练习作业？
这当然是可以的，我们会与讲师进行沟通。作业后续可能还有答疑环节，这部分活动目前暂定在QQ群进行。
是否可以对想要入门的同学多一点的照顾？
这是工具人一直争取的事，初步设计暑校的时候是没有前置课程的，但是工具人觉得这样可能会把很大一部分人排除在外，因此给大家贴心准备了相关前置课程。事实证明确实是这样，因为从问卷的情况来看熟悉类型论的人只有仅仅的%10。
是否可以充分考虑不同领域方向的听众？
目前，数学系和计算机系的同学几乎分别占了一大半，我们在尽力平衡talks的相关性，可以看到talks里面有各自领域的东西。
Infinity Type Café是怎样一个组织？
一个大部分成员都是学生的组织。特别感谢那些在意见中给于我们的支持和鼓励的朋友！
Trebor
无懈可击99
Alias Qli
Github
Email
Gestellmensch
Anqur
天生万物以养人
游客账户0x0
除了课程和 talks 的在线答疑，听众也可以通过上述联系方式联系讲师答疑，或加入暑校群（QQ 群号 791437680）询问问题。寻找讲师答疑即代表您同意我们在暑校相关内容中（包括但不限于录播视频和暑校网站）公开您的问题和答疑内容。
特别演讲人
maplgebra
conway
LiangHillon
Thanks!
