The field of program optimisation and logical relations is witnessing significant developments, with a focus on enhancing the expressiveness and efficiency of existing techniques. Researchers are exploring new frameworks and methods to improve the analysis and verification of complex programs, including the use of e-graphs, differential logical relations, and trace formula implication. These advancements have the potential to revolutionize the way programs are optimised and verified, enabling the development of more efficient and reliable software systems. Noteworthy papers in this area include:

• A paper on e-graphs with bindings, which introduces a new framework for handling variable bindings in e-graphs, enabling more efficient program optimisation and reasoning.
• A paper on the metric nature of differential logical relations, which clarifies the metric properties of these relations and provides new compositional reasoning principles for program differences.
• A paper on a sequent calculus for trace formula implication, which presents a sound sequent calculus for proving implication between trace formulas, paving the way for mechanized verification of complex programs.