很想双修数学和计算机，但是只对计算机的理论部分感兴趣（lamda 演算，类型论等），有什么课程推荐吗
cy
首先，计算机这个学科工程性还是挺强的。所以如果你只对可计算性理论和计算复杂度理论感兴趣，而对任何代码都完全不感冒，那么个人认为你实际上是对某些数学分支而不是“计算机的理论部分”感兴趣。作为一个数学水平不太好的计算机学生，我对这种情况实在是爱莫能助。
反之如果你觉得 lambda 演算之类的东西比较有意思并且愿意在计算机上玩玩它，那么也许你可以尝试函数式编程 (functional programming) 和程序语言 (programming languages) 领域的知识，辅以关于形式化方法的内容。（以下推荐的课程部分来自 CS 自学指南）
- 函数式编程是一种与命令式编程（例如 C 语言）差异很大的编程范式，一般比较喜欢数学的朋友也都会比较喜欢函数式编程，并且学习函数式编程对学习程序语言和形式化都有帮助。因为我并不擅长此道，所以就不胡乱介绍了，可以选一门课：
- Haskell MOOC，依托 Haskell 语言讲授
- Cornell CS3110，依托 OCaml 语言讲授
- 程序语言（一般简称为 PL）是以设计和分析编程语言为目标的理论，实际上由若干不同的分支组成，其中就包括你提到的类型理论。由于涉及的东西多且研究人员较少，国内这方面的课程其实比较薄弱。可以看看 Stanford CS242 这门课。这门课里也有 OCaml 函数式编程，或许不需要函数式编程课作为前置基础。
- 形式化方法比较倾向于分析和验证软件的正确性，产生了一些互联网上不太出名但影响非常深远的软件系统，比如说 seL4 操作系统内核。可以看看科大黄文超老师开的 形式化方法导引 课程（没有视频但开放课件和参考资料），我看科大的同学对这门课评价相当不错。
最后，顺便找到一篇看起来不错的知乎文章：浅谈编程语言研究与程序分析 ，也许会有所帮助，祝好。
「いいね！」 2
这篇文章作者是南大一位新来的老师。在 b 站有上传静态分析的课程。
mit 双修 math eecs 不知道怎么做到的，也许全部翘课自学可以前两年学完你交开和不开的本科 5 个方向 math 课，后两年翘课自学 csdiy？
这样可能不能毕业
Type Theory is a niche field; in fact, there are not many researchers worldwide, so video courses are relatively scarce. To get started, you can begin by learning simple proof assistants ¶, such as Agda, Idris, Coq, and the currently popular Lean 4.
After gaining a basic understanding of PA, you can read some introductory texts on type theory; I recommend the following two books:
- Type Theory and Formal Proof
- Homotopy Type Theory
After that, you can look for papers in related areas to read.
「いいね！」 2