南京大学 梁红瑾
报告生成时间：2026年8月 个人主页：https://hongjin-liang.github.io 所属团队：南京大学计算机学院 PLaX（Programming Language and Systems）实验室
一、学者基本信息
| 字段 | 内容 |
|---|---|
| 姓名 | 梁红瑾（Hongjin Liang） |
| 出生年份 | 公开来源未披露 |
| 职称 | 教授、博士生导师 |
| 所属单位 | 南京大学计算机学院 |
| 实验室职务 | PLaX（Programming Language and Systems）实验室共同牵头人（与冯新宇） |
| 学术头衔 | 国家优秀青年科学基金（优青）获得者（入选年份公开来源未标注） |
| 其他任职 | POPL、PLDI、OOPSLA、ESOP、CPP、APLAS 等顶级会议常年程序委员会委员 |
| 邮箱 | hongjin@nju.edu.cn |
| 研究方向 | 程序设计语言与形式化验证（并发程序精化验证、线性一致性/终结性/进展性、Promise 语义、CRDT、随机并发程序等） |
二、教育背景与职业履历
梁红瑾的学术根脉源于中国科学技术大学。2009 年，她毕业于中国科学技术大学少年班本科；随后在中科大计算机学院继续攻读博士学位，2014 年博士毕业，博士导师为冯新宇（Xinyu Feng）教授，博士论文题为《Refinement Verification of Concurrent Programs and Its Applications》（2014）。该论文系统研究了并发程序的精化验证理论，此方向贯穿其全部学术生涯。
在职业履历上，2014 年至 2017 年，梁红瑾在中国科学技术大学计算机学院任副研究员，隶属"中国科大—耶鲁高可信软件联合研究中心"；2017 年加入南京大学计算机学院。到南京后，她与冯新宇共同牵头组建了 PLaX（Programming Language and Systems）实验室，该实验室隶属于计算机软件新技术全国重点实验室（state key laboratory），并任教授、博导。
在学术贡献上，梁红瑾以中国大陆机构在程序设计语言顶级会议上的里程碑式工作知名。其 POPL 2012 论文是中国大陆机构较早以第一署名在 POPL 发表的代表性工作。此后，她在 POPL、PLDI 等 CCF-A 类顶会上持续发表成果，在并发程序精化验证、并发对象逻辑、CRDT 抽象、Promise 语义验证等方向形成系统理论。其 TOPLAS 2014 为 POPL 2012 的期刊版。
三、学生培养情况
梁红瑾在 PLaX 长期招收和指导博士、硕士研究生。PLaX 官方成员页分成在读与校友两栏，但多数未逐一标注指导导师归属（梁红瑾单独指导、冯新宇单独指导或共同指导），本报告据成员页如实记录。
在读学生（据 PLaX 成员页）
- Yinfeng Lin：在读学生。
- Rongen Lin：在读学生，是梁红瑾、冯新宇合作 ESOP 2025 论文"Verifying Algorithmic Versions of the Lovasz Local Lemma"的首作者。
- Jinwei Liang：在读学生。
校友
- Yuwen Kuang：毕业。
- Weijie Fan（范卫杰）：毕业，是 ESOP 2025 论文重点作者之一。
- Xuyang Li（李旭阳）：毕业，从事并发与分布式系统。
- Zhaohui Li：毕业。
- Junpeng Zha（查俊鹏）：毕业，现就职于华为，是 PLDI 2022 论文（Verifying Optimizations of Concurrent Programs in the Promising Semantics）的主要作者。
- Hanru Jiang（蒋瀚如）：毕业，现就职于北京雁栖湖应用数学研究院，是 PLDI 2019 杰出论文奖论文的第一作者。
- Chunhui He（何春辉）：毕业。
- Xiaoran Zhang：毕业。
- Chao Ding（丁超）：毕业。
说明：PLaX 成员页未逐一标注每位学生的指导归属（梁红瑾或冯新宇单独指导、或共同指导），本报告不据署名或研究方向武断推定。
四、学术合作网络
4.1 PLaX 实验室内部
南京大学 PLaX 由冯新宇与梁红瑾两名教师共建，是程序设计语言的独立实验室。
冯新宇（Xinyu Feng）教授是梁红瑾最核心的合作者，也是其博士导师。两人自 2012 年起长期发表合作涵盖 POPL 2012/2016/2018、PLDI 2013/2019（杰出论文奖）/2021/2022、TOPLAS 2014、并发对象综述 2020 等。冯新宇常为资深/通讯作者。
在读与毕业生是 PLaX 的内部延伸。
组织边界：PLaX 是独立建制的程序语言实验室，与南京大学已有的软件工程/形式化方法（nju_sefm，即计算机软件研究所）治理模式不同。本报告保持 PLaX 独立，不与 nju_sefm 并归。
4.2 跨机构 / 国际合作
梁红瑾国际网络可分早期中国科大–耶鲁合作与国际 PL 共同体两个阶段：
邵中（Zhong Shao）教授（耶鲁大学）是梁红瑾国际合作的早期节点。两人在 CONCUR 2013（与 Jan Hoffmann、冯新宇合作）和 CSL-LICS 2014（与冯新宇合作）两篇论文中合作。邵中是可验证编译器（Certified Compilers）与并发精化方向的重要学者。梁红瑾在中国科大副研究员期间隶属的"中国科大—耶鲁高可信软件联合研究中心"即以邵中为耶鲁侧协调人建立。
Jan Hoffmann（卡内基梅隆大学，CMU）与梁红瑾在 CONCUR 2013 论文（Characterizing Progress Properties of Concurrent Objects）上有论文合作。Hoffmann 专攻资源分析与概率程序验证方向。
中国科大—耶鲁高可信软件联合研究中心（2014-2017）是梁红瑾职业早期的学术归属。
国际 PL 学术共同体：梁红瑾常年担任 POPL、PLDI、OOPSLA、ESOP、CPP 等顶级会议程序委员（见第六节），是华人学者在国际 SIGPLAN 共同体中的重要联络节点。
五、业界合作关系深度分析
5.1 产业合作
在产业合作层面，PLaX 实验室的产学研公开披露较有限。可见的主要线索是毕业生代表的重要去向、以及团队在并发程序语义（Promise、CRDT 抽象等）方面的理论积累。但梁红瑾或 PLaX 是否与华为存在正式合作契约，公开来源未披露，本报告不予推断。
梁红瑾作为长期学术与教学活动的开设者（如"形式语义"课程等），这些属于学术传播与教学影响力，不属于正式产业合作。
5.2 产业合作深度评估
总体而言，梁红瑾与冯新宇以基础理论研究为重心，公开信息未见与头部企业的系统产业化合作。学生毕业进入头部企业（如华为）属个人选择。PLaX 与工业界的连接以毕业生走向为主要特征，是"学术-产业"转移的观察点，尚未见实验室层面系统性产业化披露。
六、重要奖项与学术兼职
| 年份 | 奖项 / 兼职 | 说明 |
|---|---|---|
| — | 国家优秀青年科学基金 | 已列入南大计算机学院优青名单，年份待核实 |
| 2019 | PLDI 2019 杰出论文奖 | Towards Certified Separate Compilation |
| 2022 | 中国高被引学者 | 见于公开榜单，南大方向之一 |
| 2027 | OOPSLA 2027 PC | |
| 2027 | POPL 2027 PC | |
| 2024 | PLDI 2024 PC | |
| 2022 | PLDI 2022 PC | |
| 2019 | PLDI 2019 PC 与 POPL 2019 PC | |
| 2022 | POPL 2022 PC | |
| 2025 | ESOP 2025 PC | |
| 2021 | ESOP 2021 PC | |
| 2022 | CPP 2022 PC | |
| 2021 | CPP 2021 PC | |
| 2020 | CPP 2020 PC | |
| 2023 | APLAS 2023 PC | |
| 2023 | OOPSLA 2023 PC |
七、Connection 圈层总结
梁红瑾的学术网络以团队精练、理论扎实为特征，依托 PLaX 平台，可分为四个圈层：
核心圈层（导师+长期合作伙伴）：冯新宇——博士导师、几乎全部代表作合作者、PLaX 共建者。
第二圈层（学生与团队）：在读学生三位、校友九位，成果外溢到头部企业与科研院所。
第三圈层（跨机构 / 国际）：早期中科大—耶鲁合作经验（邵中等），及国际 PL（SIGPLAN）共同体（常年程序委员）。
第四圈层（体系与边界）：PLaX 为独立建制的程序设计语言实验室（隶属国重实验室），与既有软件工程/形式化方法（nju_sefm）体系不同，不并入后者。正式产业化合作公开信息有限，待后续补充。
总体而言，梁红瑾以并发程序精化与语义验证为主线，与冯新宇构筑起具有纯理论风格的 PLaX 独立实验室（程序设计语言体系），面向国际 SIGPLAN 共同体长期参与，是一个在并发验证（Promise、CRDT、并发对象逻辑）等方向上积累了系统理论、并持续与国际（耶鲁—卡内基梅隆）合作的重要程序语言学家与独立建设者。