The field of programming languages and automated reasoning is witnessing significant developments, with a focus on designing robust frameworks that guarantee crucial properties such as runtime efficiency and termination. Researchers are exploring innovative approaches to program verification, synthesis, and analysis, leveraging techniques such as static type systems, lifted inference, and higher-order logic programming. Noteworthy papers in this area include: A Programming Language for Feasible Solutions, which introduces a new imperative programming language that ensures polynomial time complexity by design. Faster Lifting for Ordered Domains with Predecessor Relations, which devises a novel algorithm for lifted inference on ordered domains, achieving exponential speedups. The Power of Negation in Higher-Order Datalog, which establishes tight connections between Higher-Order Datalog and complexity classes, highlighting an interesting trade-off between order and non-determinism. Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types, which proposes a novel approach to satisfiability checking of Constrained Horn Clauses over Algebraic Data Types, outperforming state-of-the-art solvers.