| Monday 17. July | Tuesday 18. July | Wednesday 19. July | Thursday 20. July | Friday 21. July |
---|

8:30 | | | | | |

9:00 | OpenMath | MathUI | [I3]Grant Passmore. *Formal Verification of Financial Algorithms, Progress and Prospects* | [I2]Przemyslaw Chojecki. *DeepAlgebra - an outline of a program* | [M4]William Farmer. *Theory Morphisms in Church's Type Theory with Quotation and Evaluation* | [I1]Alan Bundy. *Reformation: A Generic Algorithm for Repairing Faulty Logical Theories* |

9:30 | [M9]Michael Kohlhase, Thomas Koprucki, Dennis Müller and Karsten Tabelow. *Mathematical Models as Research Data via Flexiformal Theory Graphs* |

10:00 | Coffee | Coffee | Coffee | Coffee | Lunch |

10:30 | OpenMath | MathUI | [C1]William Farmer and Jacques Carette. *Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study* | [M6]Andreas Holmstrom and Torstein Vik. *Zeta types and Tannakian symbols as a method for representing mathematical knowledge* | [S2]Jan Jakubuv and Josef Urban. *ENIGMA: Efficient Learning-based Inference Guiding Machine* | [D1]Patrick Ion and Stephen Watt. *The Global Digital Mathematics Library and The International Mathematical Knowledge Trust* |

11:00 | [C3]Franck Slama and Edwin Brady. *Automatically Proving Equivalence by Type-Safe Reflection* | [M10]Zohreh Shams, Mateja Jamink, Gem Stapleton and Yuri Sato. *Reasoning with Concept Diagrams about Antipatterns in Ontologies* | [S3]Ekaterina Komendantskaya and Jónathan Heras. *Proof mining with dependent types* | [D2]Olivier Labbe and Thierry Bouche. *The New Numdam platform* |

11:30 | [W3]Alexander Maletzky. *A New Reasoning Framework for Theorema 2.0* | [M3]Joseph Corneli, Ursula Martin, Dave Murray-Rust and Alison Pease. *Towards mathematical AI via a model of the content and process of mathematical question and answer dialogues* | [S5]Usman Sanwal and Umair Siddique. *Combining Refinement and Signal-Temporal Logic for Biological Systems* | [D4]Wolfram Sperber and Michael Kohlhase. *Software Citations, swMATH, and Beyond* |

12:00 | [C2]Alexander Maletzky and Wolfgang Windsteiger. *The Formalization ofVickrey Auctions: A Comparison of Two Approaches in Isabelle and Theorema* | [M8]Andrea Kohlhase, Michael Kohlhase and Michael Fürsich. *Visual Structure in Math Expressions* | [S4]Adnan Rashid and Osman Hasan. *Formalization of Transform Methods using HOL Light* | [D3]Dennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase and Florian Rabe. *Classification of Alignments between Concepts of Formal Mathematical Systems* |

12:30 | Lunch | Lunch | Lunch | Lunch | Lunch |

14:00 | Doctoral Programme | OpenMath | MathUI | [M2]Howard Cohl, Moritz Schubotz, Abdou Youssef, André Greiner-Petter, Jürgen Gerhard, Bonita V. Saunders, Marjorie A. McClain, Joon Bang and Kevin Chen. *Semantic Preserving Bijective Mappings of Mathematical Formulae between Word Processors and Computer Algebra Systems* | Excursion | [S7]Abdou Youssef. *Part-of-Math Tagging and Applications* | |

14:30 | [M5]Ian Ford. *Semantic Representation of General Topology in the Wolfram Language* | [S1]Nathan Carter and Kenneth Monks. *A Web-Based Toolkit for Mathematical Word Processing Applications with Semantics* |

15:00 | [W1]Catherine Dubois, Thérèse Hardin, François Pesseaux and Renaud Rioboo. *Proving mathematical libraries: FoCaLiZe polynomials* | [S6]Moritz Schubotz, Norman Meuschke, Thomas Hepp, Howard Cohl and Bela Gipp. *VMEXT: A Visualization Tool for Mathematical Expression Trees* |

15:30 | Coffee | Coffee | [W4]Adam Naumowicz. *Towards Standardized Mizar Environments* |

16:00 | Doctoral Programme | OpenMath | MathUI | [M1]Marco B. Caminati and Juliana Küster Filipe Bowles. *A Verified Algorithm Enumerating Event Structures* | Coffee |

16:30 | [M7]Cezary Kaliszyk and Karol Pąk. *Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic* | Business Meeting |

17:00 | [W2]Carlos E. Freites. *Mathdialog: a contextual ZFC syntactical game* |

17:30 | [W5]Patrick Ion and Eric Weisstein. *The Special Function Concordance* |