 Monday 25. July  Tuesday 26. July  Wednesday 27. July  Thursday 28. July  Friday 29. July 

8:30  Registration  Registration  Registration  Registration  Registration 
Room  2048  2001  Aula  Aula  Aula  Aula  2001  Aula  2048 
9:00  FM4M
Invited Talk: [F1]Chad Brown. Invited talk: Developments, Libraries and Automated Theorem Provers ( Slides)
Chair: Naumowicz  C. Sacerdoti
Coen [I2]Claudio Sacerdoti Coen. Towards Extensible Algorithmic Mathematical Knowledge ( Slides) Chair: Kohlhase  John Harrison [I1] Chair: Brown  Nicolas Thiery [I3]Nicolas Thierry. Infrastructure for generic code in SageMath: categories, axioms, constructions ( Slides) Chair: Sacerdoti Coen    
10:00  Coffee  Coffee  Coffee  Coffee  Coffee 
10:30  Doctoral Program
[DP1]Marek Janasz. Automated theorem proving for elementary geometry [DP2]Dennis Müller. Knowledge Management across Formal Libraries [DP3]Moritz Schubotz. Augmenting Mathematical Formulae for More Effective Querying & Presentation ( Slides) [DP4]Théo Zimmermann. Design and development of a tool based on Coq to write and format mathematical proofs
 MathUI
[M1]Lucius Schoenbaum. Towards Visual Type Theory as Mathematical Tool and Mathematical User Interface [M2]Andrea Kohlhase and Michael Fürsich. Understanding Mathematical Expressions: An EyeTracking Study
 FM4M
[F2]Adam Grabowski. Tarski's geometry and Euclidean plane in Mizar [F3]Mario Carneiro. Formalization of the prime number theorem and Dirichlet's theorem ( Slides) [F4]Karol Pąk. Topological Foundations for a Formal Theory of Manifolds
 MKM
[R5]Adam Naumowicz and Radosław Piliszek. Accessing the Mizar Library with a Weakly Strict Mizar Parser [R19]Chad Brown and Josef Urban. Extracting HigherOrder Goals from the Mizar Mathematical Library ( Slides) [W33]Karol Pąk. Lemma Extraction Criteria Based on Properties of Theorem Statements [W47]Karol Pąk and Aleksy Schubert. The impact of proof steps sequence on proof readability – experimental setting
Chair: Farmer
 Projects & Surveys
[R21]PaulOlivier Dehaye, Mihnea Iancu, Michael Kohlhase, Alexander Konovalov, Samuel Lelièvre, Dennis Müller, Markus Pfeiffer, Florian Rabe, Nicolas M. Thiéry and Tom Wiesing. Interoperability in the OpenDreamKit Project: The MathintheMiddle Approach [R39]Waqar Ahmed, Osman Hasan and Sofiene Tahar. Formal Dependability Modeling and Analysis: A Survey ( Slides)
Chair: Ion
 CALCULEMUS
[R4]Alexander Maletzky. Mathematical Theory Exploration in Theorema: Reduction Rings [R11]Ken'Ichi Kuga, Manabu Hagiwara and Mitsuharu Yamamoto. Formalization of Bing's shrinking method in geometric topology [R31]Erika Ábrahám, Bernd Becker, James H. Davenport and Pascal Fontaine. SCsquare: Satisfiability Checking meets Symbolic Computation [R36]Muhammad Qasim, Osman Hasan, Maissa Elleuch and Sofiene Tahar. Formalization of Normal Random Variables in HOL ( Slides)
Chair: Naumowicz
 OpenMath  Mizar HandsOn Tutorial  MMT
Tutorial

11:30  Systems & Data
[R18]Jan Jakubuv and Josef Urban. Extending E Prover with Similarity Based Clause Selection Strategies [R42]Artur Kornilowicz. Enhancement of Mizar Texts with Transitivity Property of Predicates
Chair: Ion

12:30  Lunch  Lunch  Lunch  Lunch  Lunch 
14:00  OpenMath
Agenda, Standards Discussion
[O0]Michael Kohlhase. The 29th OpenMath Workshop, Agenda/Planning [O1]Tom Wiesing. An Overview over SCSCP
 MathUI
[M3]Paul Libbrecht and Matija Lokar. The plain text trap when copying mathematical formulae [M4]Juan LaoTebar, Francisco Alvaro and Daniel Marqus. Proposal for Coexistence of Mathematical Handwritten and Keyboard Input in a WYSIWYG Expression Editor
 FM4M/ThEdu
Invited Talk: [F6]Aleksy Schubert. Invited talk: On Differences in Proofs Between Intuitionistic and Classical Logic
[T1]Walther Neuper. LucasInterpretation from Users’ Perspective ( Slides)
 MKM
[R8]William Farmer. Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics ( Slides) [W1]Mario Carneiro. Models for Metamath ( Slides) [W44]Andreas Holmstrom. A first step towards automated conjecturemaking in higher arithmetic geometry
Chair: Rabe
 Excursion  DML
[R32]Olaf Teschke and Fabian Müller. Progress of selfarchiving within the DML corpus, with a view toward community dynamics [W10]Wolfram Sperber, Hagen Chrapary and Wolfgang Dalitz. swMATH  challenges, next steps, and outlook ( Slides) [W38]Hiroyuki Okazaki and Yuichi Futa. Formalization of Polynomially Bounded and Negligible Functions using the ComputerAided ProofChecking System Mizar
Chair: Davenport
 Tetrapod  Mizar HandsOn Tutorial 
15:30  Coffee  Coffee  Coffee  Coffee 
16:00  OpenMath
[O2]Bruce Miller. Drafting DLMF Content Dictionaries [O3][O4][O5]Michael Kohlhase. Towards OpenMath 2.1 or 3; Issues and Criteria [O6]Michael Kohlhase. Sequence Variables in OpenMath
 MathUI
[M5]Tom Wiesing and Felix Schmoll. KAT: an Annotation Tool for STEM Documents [M6]Ion Toloaca and Michael Kohlhase. Notationbased Semantification
 FM4M/ThEdu
[T2]Walther Neuper. Rigor of TP in Educational Engineering Software ( Slides) [F5]Artur Korniłowicz. Registrations vs Redefinitions in Mizar [F7]Adam Naumowicz. Linking to Compound Conditions in Mizar
 MKM
[W23]Thibault Gauthier, Cezary Kaliszyk and Josef Urban. Initial Experiments with Statistical Conjecturing over Large Formal Corpora [W24]Cezary Kaliszyk, Michael Kohlhase, Dennis Müller and Florian Rabe. A Standard for Aligning Mathematical Concepts [W50]Denis Rochau, Michael Kohlhase and Dennis Müller. FrameIT Reloaded: Serious Math Games from Modular Math Ontologies
Chair: Urban
 DML
[W45]Moritz Schubotz, David Veenhuis and Howard Cohl. Getting the units right ( Slides) [W48]Moritz Schubotz and Alan Sexton. A Smooth Transition to Modern mathoidbased Math Rendering in Wikipedia with Automatic Visual Regression Testing ( Slides)
Chair: Sorge
 Tetrapod  Mizar HandsOn Tutorial 
17:30  General Meeting   Track Meetings?  Business Meeting  
19:00   Conference Dinner 