Chair: Dennis Müller

• 9:30: Caitlin D'Abrera, Rajeev Gore. Verified Synthesis of (Very Simple) Sahlqvist Correspondents via Coq.
• 10:00: Petros Papapanagiotou, Jacques Fleuriot. Object-level reasoning with logics encoded in HOL Light.
• 10:30: Navid Roux, Florian Rabe. Diagram Operators in a Logical Framework.