Introduction to the Special Section on ESOP 2020

Abstract

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.