跳转到内容
Jason's Study

编译器 / 编程语言理论 · 论文 · 第 1 组

待复核

返回论文全景索引

本分块共 100 条，稳定上限为 100 条。

论文Slug难度可信状态简介
Adapton — 增量计算adaptonunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Agda — 让你写代码的同时把数学也证明了agda-norellunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
ALGOL 60 — BNF 与块结构algol-60unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Andersen 指针分析 — 让编译器自己算出 p 可能指向谁andersen-pointer-analysisunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Apron — 把区间/八边形/多面体塞进同一个插槽apron-2009unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
ASTRÉE 分析器 — 让飞机控制代码的静态分析做到零警告astreeunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Backus FP 1978 — 把程序从赋值循环里解放出来backus-fp-1978unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
双向类型检查 — 推断和检查两个方向交替前进bidirectional-typingunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
CakeML — 从源码到机器码每一步都被数学证明的 ML 编译器cakemlunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Calculus of Constructions — 让程序和数学证明共用一种语言calculus-of-constructionsunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Call-by-Need Lambda Calculus — 给惰性求值一套真正的演算call-by-need-1995unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Chaff 2001 — 把 CDCL 工程化的两个杀手锏chaff-2001unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Chaitin 图染色寄存器分配 — 把硬件资源问题翻译成数学问题chaitin-graph-coloringunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
CI Effects — 持续集成不是免费午餐，价值看实现细节ci-effectsunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Coeffects — 让类型系统追踪「需要多少上下文」coeffect-petricekunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
CompCert — 每条优化都被数学证明保持语义的 C 编译器compcertunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Compiler Error Messages — 让编译报错有用compiler-errorsunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Cousot 抽象解释 — 给静态分析一套统一数学框架cousot-abstract-interpretationunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Cousot-Halbwachs 凸多面体域 — 让分析器自己发现变量间的线性关系cousot-halbwachs-polyhedra-1978unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
CRDT JSON — 协同编辑 JSON 数据结构crdt-jsonunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
CSP — 进程之间只许喊话不许共用内存csp-hoare-1978unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
CUTLASS — 把 SOTA GEMM 拆成可组合的 C++ 模板层级cutlass-2020unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Davis-Putnam 1960 — 让机器自动判断一堆逻辑式能不能同时成立davis-putnam-1960unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
DDlog (Differential Datalog) — 输入只改一条，引擎只算受影响的那一小块differential-datalogunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Go To Statement Considered Harmful — 控制流程的清晰优先级dijkstra-goto-1968unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Doligez-Leroy Concurrent GC — ML 线程运行时里的准实时垃圾回收doligez-leroy-concurrent-gcunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
DPLL 1962 — 把”逻辑判定”从内存爆炸救成栈式回溯dpll-1962unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
DSPy — 把 prompt 写成签名，让编译器替你调dspyunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
E-Path — 把 CFG 优化从单行通道改成候选池e-path-egraphunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Earley Parser — 一个表能解析任何 CFG 的通用解析器earley-parserunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
代数效应（Algebraic Effects）effect-handlersunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Egglog — 把 Datalog 和等式饱和合成一台推理引擎egglog-incremental-2026unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Erlang OTP — 容错并发系统设计erlang-otpunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Feautrier 多面体调度 — 把循环并行化变成解几何方程feautrier-polyhedralunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Frank — 让 effect handler 写得就像普通函数frank-effectsunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
F* — 把依赖类型、SMT 自动化、副作用追踪揉到一门语言里fstarunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
G1 Garbage-First — 给暂停时间设个预算的垃圾回收器g1-collectorunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
GADT — 让构造子告诉编译器”我返回的是更精确的类型”gadt-pjonesunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
博弈论语义与 PCF — 把程序解释成两个人轮流下的对话棋game-semantics-pcfunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
GraalVM Truffle — 写一棵会自我特化的语法树就能自动得到 JITgraalvm-truffleunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
渐进类型 — 让动态和静态类型在同一份代码里共存gradual-typingunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Granule — 让类型系统同时数次数、看安全级、追副作用granuleunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Halide — 把”算什么”和”怎么算”分开写halideunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Helium — 让类型错误说人话的教学版 Haskellhelium-type-errorsunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Hewitt Actor 模型 — 把计算拆成一群只会发消息的小邮筒hewitt-actor-modelunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Hindley-Milner — 编译器自己猜变量类型hindley-milnerunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Hoare CSP 1978 — 把并发看成会对话的小程序hoare-csp-1978unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
HotSpot Server Compiler — JVM 在运行时把热点 Java 代码翻译成飞快的本地码hotspot-server-compilerunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Why FP Matters — 函数式真正赢在能拆能粘hughes-fp-mattersunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Idris — 让依赖类型从证明助理变成通用编程语言idris-bradyunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Bi-Abduction — 让静态分析自动猜出函数缺什么前提infer-biabductionunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Kahn 自然语义 — 用一棵推理树说清楚程序求值kahn-natural-semanticsunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Kami — 在 Coq 里造硬件并自动编译到 Verilogkami-2017unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Kildall 数据流框架 — 用一套格论统一所有全局编译优化kildall-dataflowunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Knuth LR(k) — 编译器自己读懂语法的算法knuth-lr-1965unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
LACUNA — 把 AI agent 的行动变成编译器先检查的程序洞lacuna-program-holesunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
DeRemer LALR(1) — 把 LR 表压到能用大小lalr-deremerunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Landin SECD — 第一台机械求值 lambda 表达式的抽象机器landin-secdunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Lean 4 — 用 Lean 重写的 Lean，让数学家和程序员共用一种语言lean-proverunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Lean Tactics — 让证明助手把”写证明”当成写程序lean-tacticsunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Lerner 组合数据流 — 让小优化互相喂招lerner-seminalunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Linear Scan 寄存器分配 — 把图染色换成单趟扫描，给 JIT 用linear-scan-reg-allocunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
线性类型（Linear Types）linear-typesunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Liquid Types — 让编译器自己推导出”哪些值才合法”liquid-typesunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Liskov 抽象数据类型 — 用操作而不是存储形状定义数据liskov-abstraction-1974unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
LLVM — 模块化编译器框架llvmunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Local Type Inference — 编译器只看相邻节点也能推出类型local-type-inferenceunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
GRASP 1996 — 让 SAT 求解器从冲突里学到东西marques-silva-grasp-1996unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Martin-Löf 直觉主义类型论 — 让”证明”和”程序”变成同一件事martin-lof-ittunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
McCarthy LISP 1960mccarthy-lispunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
MetaML — 让你显式地写”先生成代码、再跑代码”metaml-multi-stageunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
MileStone — 让编译器按能耗预算自己排优化顺序milestone-phase-orderunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
π-演算 — 让通道名本身能在通道里流动milner-pi-calculusunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Miné 八边形抽象域 — 在区间和多面体之间的甜点mine-octagon-2006unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
MiniSat 2003 — 600 行 C++ 把 CDCL 写成教科书minisat-2003unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
MLIR — 给编译器一套乐高，每层抽象都能搭自己的方言mlirunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Mycroft 严格性分析 — 编译器替你判定哪些参数能”先算”mycroft-strictnessunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Nelson-Oppen 1979 — 让多个判定程序坐下来交换”我刚发现 a=b”nelson-oppen-1979unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Nieuwenhuis-Oliveras-Tinelli 2006 — 给 SMT 求解器写一套数学规则书nieuwenhuis-dpll-t-2006unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Jones-Gomard-Sestoft 1993 — Partial Evaluation 与自动程序生成partial-evaluation-jonesunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
PassNet — 让大模型给图编译器写优化 passpassnet-graph-compilerunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
PEG / Packrat — 用’有序选择’+‘记忆化’写线性时间解析器peg-packrat-fordunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Peyton Jones STG — 让 Haskell 的 lazy 在普通 CPU 上跑得快peyton-jones-stgunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Plotkin SOS — 用规则讲清楚程序”走一步”是什么plotkin-sosunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Pottier LR(1) Reachability — 让 LR 解析器的错误消息覆盖完整pottier-merrunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Prolog 的诞生 — 让逻辑式子直接当程序跑prolog-colmerauerunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Push-Pull FRP — Functional Reactive Programming 实用化push-pull-frpunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
PyPy meta-tracing JIT — 给解释器加一次 JIT，所有用它的语言一起加速pypy-tracing-jitunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
REALM — 把检索器和 BERT 一起预训练的第一篇论文realmunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Refinement Types for ML — 让程序员告诉编译器”哪些子集才合法”refinement-types-1991unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Reps-Horwitz-Sagiv IFDS — 把跨过程分析变成图上找路reps-ifdsunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Reynolds Definitional Interpreters — 用一种语言去定义另一种语言reynolds-definitional-interpretersunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Separation Logic — 把 Hoare 逻辑扩到带指针的程序reynolds-separation-logicunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Row Polymorphism — 让函数不必知道 record 的全部字段row-polymorphism-remyunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Sagiv 参数化形状分析 — 用三值逻辑证明链表树仍是链表树sagiv-shape-analysisunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Salsa / Adapton — 让程序只重算”真的变了”的那一小块salsa-adaptonunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Scala Macros — 让 Scala 在编译期把方法调用替换成任意代码scala-macrosunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Scott-Strachey 指称语义 — 给程序找一个独立于实现的数学含义scott-strachey-denotationalunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Self-Adjusting Computation — 输入小幅变化时只重算受影响的那部分self-adjustingunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
SELF Customization — 给每种”调用者类型”现场打一份方法self-customizationunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。

下一组