List of Events

Invited Talks

• [I1] Alan Bundy. Reformation: A Generic Algorithm for Repairing Faulty Logical Theories
• [I2] Przemyslaw Chojecki. DeepAlgebra - an outline of a program
• [I3] Grant Passmore. Formal Verification of Financial Algorithms, Progress and Prospects

Calculemus

• [C1] William Farmer and Jacques Carette. Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study
• [C2] Alexander Maletzky and Wolfgang Windsteiger. The Formalization ofVickrey Auctions: A Comparison of Two Approaches in Isabelle and Theorema
• [C3] Franck Slama and Edwin Brady. Automatically Proving Equivalence by Type-Safe Reflection

Digital Mathematical Libraries

• [D1] Patrick Ion and Stephen Watt. The Global Digital Mathematics Library and The International Mathematical Knowledge Trust
• [D2] Olivier Labbe and Thierry Bouche. The New Numdam platform
• [D3] Dennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase and Florian Rabe. Classification of Alignments between Concepts of Formal Mathematical Systems
• [D4] Wolfram Sperber and Michael Kohlhase. Software Citations, swMATH, and Beyond

Mathematical Knowledge Management

• [M1] Marco B. Caminati and Juliana Küster Filipe Bowles. A Verified Algorithm Enumerating Event Structures
• [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
• [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
• [M4] William Farmer. Theory Morphisms in Church's Type Theory with Quotation and Evaluation
• [M5] Ian Ford. Semantic Representation of General Topology in the Wolfram Language
• [M6] Andreas Holmstrom and Torstein Vik. Zeta types and Tannakian symbols as a method for representing mathematical knowledge
• [M7] Cezary Kaliszyk and Karol Pąk. Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic
• [M8] Andrea Kohlhase, Michael Kohlhase and Michael Fürsich. Visual Structure in Math Expressions
• [M9] Michael Kohlhase, Thomas Koprucki, Dennis Müller and Karsten Tabelow. Mathematical Models as Research Data via Flexiformal Theory Graphs
• [M10] Zohreh Shams, Mateja Jamink, Gem Stapleton and Yuri Sato. Reasoning with Concept Diagrams about Antipatterns in Ontologies

Systems & Projects

• [S1] Nathan Carter and Kenneth Monks. A Web-Based Toolkit for Mathematical Word Processing Applications with Semantics
• [S2] Jan Jakubuv and Josef Urban. ENIGMA: Efficient Learning-based Inference Guiding Machine
• [S3] Ekaterina Komendantskaya and Jónathan Heras. Proof mining with dependent types
• [S4] Adnan Rashid and Osman Hasan. Formalization of Transform Methods using HOL Light
• [S5] Usman Sanwal and Umair Siddique. Combining Refinement and Signal-Temporal Logic for Biological Systems
• [S6] Moritz Schubotz, Norman Meuschke, Thomas Hepp, Howard Cohl and Bela Gipp. VMEXT: A Visualization Tool for Mathematical Expression Trees
• [S7] Abdou Youssef. Part-of-Math Tagging and Applications

Work in progress

• [W1] Catherine Dubois, Thérèse Hardin, François Pesseaux and Renaud Rioboo. Proving mathematical libraries: FoCaLiZe polynomials
• [W2] Carlos E. Freites. Mathdialog: a contextual ZFC syntactical game
• [W3] Alexander Maletzky. A New Reasoning Framework for Theorema 2.0
• [W4] Adam Naumowicz. Towards Standardized Mizar Environments
• [W5] Patrick Ion and Eric Weisstein. The Special Function Concordance

Business Meetings

• [B1] Business Meeting