金枪鱼之夜：Automaton is all you need?

[Xiaoyi Liu]

Dear Tunars,

在五一假期（真的有假期嘛？）前夕，我们计划了一次 Tunight 活动。本次活动我们邀请到了 Tunight 的老朋友，PL 专家朱俸民老师，为我们分享他的最新研究成果。

---

字符串和字符串操作在真实世界的编程任务中随处可见。主流编程语言的类型系统往往只用一种统一的String类型来表示任意字符串。为了更好的区分>具有不同结构和语义的字符串（如 IPv4 v.s. IPv6 address），我们可以引入正则语言作为refinement type进行更加精确的分析和验证。其难点在于>如何对正则语言和常见的字符串操作（如substring, contains, split）进行高效的推理。提起正则语言，人们往往会自然联想到自动机。但这种通用>的、能登大雅之堂的理论方法复杂度较高。本次讲座将从Brzozowski derivatives的视角重新审视正则语言的推理问题，介绍一种不使用自动机，而完>全通过操作正则表达式的抽象语法树的新方法。它可以用来验证Python的IPv6 address parser。

---

活动信息：

* 活动主页：https://tuna.moe/event/2026/refinement-str/

* 主讲人：朱俸民 (https://paulz.me/)
* 时间：2026/04/29（校历第十周周三） 19:00 UTC +08:00
* 活动形式：线下 + 线上会议 + 直播
  * 地点：自强科技楼 5505
  * 线上会议：腾讯会议 883-487-008 密码 260429 (https://meeting.tencent.com/dm/XkGauwPoxt3k)

  * 直播链接：https://youtube.com/live/1Mm59sxlX_g

欢迎大家一起来玩！

喵喵