The field of programming language semantics and verification is witnessing significant developments, with a focus on innovative approaches to reasoning about loops, linear logic, and catalytic computation. Researchers are exploring new perspectives on assigning meaning to proofs, simplifying the theory of loops, and settling open questions in catalytic computation. Notable papers in this area include those that propose a proof-theoretic approach to the semantics of classical linear logic, collapse catalytic classes, and introduce a game-based approach to model-checking for HyperQPTL. These advancements have the potential to improve the efficiency and effectiveness of programming language verification and validation. Noteworthy papers include:

• A paper that proposes a proof-theoretic approach to the semantics of classical linear logic, extending the framework to the classical case and presenting a proof-theoretic approach to the semantics of the multiplicative-additive fragment of linear logic.
• A paper that collapses catalytic classes, giving an optimal reduction from catalytic space with additional resources to the corresponding non-catalytic space classes and settling almost all questions regarding randomized and non-deterministic catalytic computation.