一句话：介绍 ESOP 2020 特刊背景，并概述两篇受邀扩展论文：安全编译与 Rust 验证。
本文是 TOPLAS 的 ESOP 2020 专题导言。ESOP 是 ETAPS 会议之一，关注程序语言与系统的规约、设计、分析和实现。ESOP 2020 原定于 2020 年 4 月 27–30 日在都柏林举行，但因 COVID-19 疫情先推迟后取消；程序委员会此前已选出 27 篇会议论文，并邀请其中若干优秀论文扩展投稿至本专题。本期收录两篇扩展论文：一篇研究放宽的编译器正确性定义，用源/目标 trace 及任意关系连接，推广到 hyperproperty 与安全编译；另一篇 RustHorn 提出基于 CHC 的 Rust 程序验证技术，利用 Rust 类型系统的线性保证避免显式内存表示，并已适配其他验证方法。
The European Symposium on Programming (ESOP) is one of the European Joint Conferences on Theory and Practice of Software (ETAPS). It is devoted to fundamental issues in the specification, design, analysis, and implementation of programming languages and systems. ESOP 2020 was originally scheduled to be held April 27–30, 2020, in Dublin, Ireland. However, the COVID-19 pandemic forced the organizers to first postpone and then cancel the conference. Before this decision was made, the program committee had selected 27 papers to appear at the conference. Of those, the committee selected an outstanding few and invited the authors to submit extended versions of their ESOP papers to this special section of TOPLAS. This issue includes two of those extended papers: In “Trace-relating Compiler Correctness and Secure Compilation,” Carmine Abate, Roberto Blanco, S, tefan Ciobâcă, Deepak Garg, Cătălin Hrit,cu, Marco Patrignani, Éric Tanter, and Jérémy Thibault study a relaxed compiler correctness definition, which uses source and target traces drawn from potentially different sets and connected by an arbitrary relation. This approach generalizes to hyperproperties and secure compilation. In “RustHorn: CHC-based Verification for Rust Programs,” Yusuke Matsushita, Takeshi Tsukada, and Naoki Kobayashi present a verification technique for Rust programs that uses the linearity guarantees provided by Rust’s system type to avoid an explicit representation of the memory. This approach is explored in the context of constrained Horn clauses and has already been adapted to other verification approaches. I thank the authors and reviewers for all their effort in producing and reviewing these papers. I also gratefully acknowledge the support of the TOPLAS editor-in-chief, Andrew Myers, the TOPLAS editorial staff, and the ESOP 2020 program committee for their help in selecting the invited papers.