编程语言

学习列表

• 定理证明：Lean 4
• 学术特性：Haskell
• Ocaml (方言)
• 阴谋：Schemes

语法

• 同像 Bicameral

演算

基础

• 小步/大步操作语义
• 指称语义

求值策略

• Call by value
• Call by name
• Call by need
• Call by push value
• Call by text? (maybe fexpr)

进阶

• 性质
• 证明方法

Lambda Calculus

• Binary Lambda Calculus

逻辑

类型系统

基础

• 复习/精读 TAPL 最后几章
• 行多态
• Lambda Cube

进阶

• Hindley-Milner 类型系统
• 双向类型系统
• 渐进类型

研读

• 类型精化（Elaboration Zoo）
• 不相交多态
• 动态语言类型推断
• 代数子类型

数据类型

• Abstract DTs
• ADT/Inductive Type
• Coinductive Types

计算

续延/代数式副作用

基础

• Effects/Coeffects

研读

• Sequent Calculus
• Evidence Passing

其他

• 模态效应类型

抽象理论

研读

• T/S-Expressiveness
• Abstractive Power

元编程

宏

• 一等宏
• 嵌入式卫生宏

Staging

文法

基础

• CFG
• PEG
• Chumsky Grammar

可拓展文法

• Attribute Grammar
• Recursive Adaptive Grammar

资源管理

基础

• 区域
• 所有权
• 内存模型
• Proper Tail Recursion
• 废料收集（及其嵌入）

研读

• 线性/仿射类型
• 借用检查
• 模态

其他

• 代际引用

构建

构建系统

• Nix/Guix（可重现性）

编译

解析

• 增量解析
• 解析器组合子
• 无损语法树
• 红绿树
• 可逆语法

语言定义

• Nanopass Languages
• Trees that grows

部分求值

增量编译

研读

• Scope Graphs

编辑器

结构化编辑器

语言服务

函术珠玑

Pretty Printing

表达式问题

• Datatypes a la carte
• Tagless final
• Trees that grow

可重放性

• Lisp image

操作系统

安全

• 能力