Types -- Compilation Semantics for a Programming Language with Versions -- What Types are Needed for Typing Dynamic Objects? A Python-based Empirical Study -- Types and Semantics for Extensible Data Types -- Functional Languages -- A Diamond Machine for Strong Evaluation -- Proofs as Terms, Terms as Graphs -- Typed Non-determinism in Functional and Concurrent Calculi -- Interactive Theorem Proving -- A Fresh Look at Commutativity: Free Algebraic Structures via Fresh Lists -- Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions -- Experimenting with an Intrinsically-typed Probabilistic Programming Language in Coq -- Verification -- Towards a Framework for Developing Verified Assemblers for the ELF Format -- Transport via Partial Galois Connections and Equivalences -- Argument Reduction of Constrained Horn Clauses Using Equality Constraints -- Static Analysis and Testing -- Incorrectness Proofs for Object-Oriented Programs via Subclass Reflection -- m-CFA Exhibits Perfect Stack Precision -- TorchProbe: Fuzzing Dynamic Deep Learning Compilers.