The field of programming language semantics and verification is witnessing significant developments, with a focus on improving the expressiveness and efficiency of programming languages. Researchers are exploring new techniques to enhance the verification of programs, including the use of copatterns, generic programming, and continuation-passing style transformations. Additionally, there is a growing interest in the study of automata over infinite words, with a shift towards transition-based acceptance. Noteworthy papers in this area include: Reachability is Decidable for ATM-Typable Finitary PCF with Effect Handlers, which presents a novel continuation-passing style transformation to prove the decidability of reachability for a class of programs. Big-Stop Semantics: A Simple Way to Get the Benefits of Small-Step Semantics in a Big-Step Judgment, which introduces a new semantics that captures diverging computations without introducing error states. Efficient Learning of Weak Deterministic B"uchi Automata, which presents an efficient Angluin-style learning algorithm for weak deterministic B"uchi automata.