| 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 |
