List of Events

Invited Talks

• [Invited Talk Jim Pitman] Jim Pitman. Towards a Global Digital Mathematics Library (Monday, 14:00-15:00, Meridian Room)
• [Invited Talk Richard Zanibbi] Richard Zanibbi (with Awelemdy Orakwue). Math Search for the Masses: Multimodal Search Interfaces and Appearance-Based Retrieval (DOI) (Tuesday, 14:00-15:00, Meridian Room)
• [Invited Talk Tobias Nipkow] Tobias Nipkow (with Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk). Mining the Archive of Formal Proofs (Thursday, 14:00-15:00, Meridian Room)
• [Invited Talk Leonardo de Moura] Leonardo de Moura. Formalizing mathematics using the Lean Theorem Prover (DOI) (Friday, 14:00-15:00, Meridian Room)

Calculemus

• [R1] Waqar Ahmed and Osman Hasan. Towards Formal Fault Tree Analysis using Theorem Proving (DOI) (Thursday, 15:00-15:30, Meridian Room)
• [R2] Luís Cruz-Filipe and Peter Schneider-Kamp. Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof (DOI) (Thursday, 15:30-16:00, Meridian Room)
• [R3] Evgenii Kotelnikov, Laura Kovacs and Andrei Voronkov. A First Class Boolean Sort in First-Order Theorem Proving and TPTP (DOI) (Thursday, 16:30-17:00, Meridian Room)
• [R4] Steven Obua, Jacques Fleuriot, Phil Scott and David Aspinall. Type Inference for ZFH (DOI) (Thursday, 17:00-17:30, Meridian Room)
• [R5] Florian Rabe. Generic Literals (DOI) (Friday, 15:00-15:30, Meridian Room)
• [R6] Paul Tarau. Ranking/unranking of Lambda Terms with Compressed de Bruijn Indices (DOI) (Friday, 15:30-16:00, Meridian Room)

Digital Mathematical Libraries

• [R7] Mihnea Iancu and Michael Kohlhase. A Flexiformal Model of Knowledge Dissemination and Aggregation in Mathematics (DOI) (Tuesday, 15:00-15:30, Meridian Room)

Mathematical Knowledge Management

• [R8] Serge Autexier and Dieter Hutter. Structure Formation in Large Theories (DOI) (Tuesday, 15:30-16:00, Meridian Room)
• [R9] Fulya Horozal and Florian Rabe. Formal Logic Definitions for Interchange Languages (DOI) (Tuesday, 16:30-17:00, Meridian Room)
• [R10] Mihnea Iancu and Michael Kohlhase. Math Literate Knowledge Management via Induced Material (DOI) (Tuesday, 17:00-17:30, Meridian Room)
• [R11] Bruce Miller. Strategies for Parallel Markup (DOI) (Tuesday, 17:30-18:00, Meridian Room)
• [R12] Karol Pąk. Readable Formalization of Euler's Partition Theorem in Mizar (DOI) (Thursday, 11:00-11:30, Meridian Room)
• [R13] Daniel Raggi, Alan Bundy, Gudmund Grov and Alison Pease. Automating change of representation for proofs in discrete mathematics (DOI) (Thursday, 11:30-12:00, Meridian Room)
• [R14] Qun Zhang and Abdou Youssef. Performance Evaluation and Optimization of Math-Similarity Search (DOI) (Thursday, 12:00-12:30, Meridian Room)

Projects & Surveys

• [R17] Cezary Kaliszyk, Josef Urban, Umair Siddique, Sanaz Khan-Afshar, Cvetan Dunchev and Sofiene Tahar. Formalizing Physics: Automation, Presentation and Foundation Issues (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room)
• [R19] Umair Siddique, Osman Hasan and Sofiene Tahar. Towards the Formalization of Fractional Calculus in Higher-order Logic (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room)
• [R20] Max Wisniewski, Alexander Steen and Christoph Benzmüller. LeoPARD --- A Generic Platform for the Implementation of Higher-Order Reasoners (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room)
• [R15] Grzegorz Bancerek, Czeslaw Bylinski, Adam Grabowski, Artur Kornilowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk and Josef Urban. Mizar: State-of-the-art and Beyond (DOI) (Thursday, 9:00-9:45, Meridian Room)
• [R18] Claudio Sacerdoti Coen and Ferruccio Guidi. A Survey on Retrieval of Mathematical Knowledge (DOI) (Thursday, 9:45-10:30, Meridian Room)
• [R16] Howard Cohl, Moritz Schubotz, Marjorie McClain, Bonita Saunders, Cherry Y. Zou, Azeem S. Mohammed and Alex A. Danoff. Growing the Digital Repository of Mathematical Formulae with Generic LaTeX Sources (DOI) (Friday, 17:30-18:00, Meridian Room)

Systems & Data

• [R21] Moa Johansson, Dan Rosén, Nicholas Smallbone and Koen Claessen. TIP: Tons of Inductive Problems (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room)
• [R22] Ross Moore. Semantic Enrichment of Mathematics via `tooltips' (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room)
• [R23] Kazuhisa Nakasho and Yasunari Shidama. Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room)
• [R24] Adam Naumowicz. Tools for MML Environment Analysis (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room)
• [R25] Ons Seddiki, Cvetan Dunchev, Sanaz Khan-Afshar and Sofiene Tahar. Enabling Symbolic and Numerical Computations in HOL Light (DOI) (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room)

Work in progress

• [WIP1] Bob Neveln, Bob Alps. Parsing Texts and Checking Proofs in LaTeX (Friday, 16:30-17:00, Meridian Room)
• [WIP2] Mario Carneiro. Arithmetic in Metamath, Case Study: Bertrand's Postulate (Friday, 17:00-17:30, Meridian Room)
• [WIP3] Théo Zimmermann, Hugo Herbelin. Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant (Tuesday, 18:00-18:30, Meridian Room)
• [WIP4] Pedro Quaresma, Vanda Santos, Milena Marić. A Web Environment for Geometry (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room)
• [WIP5] Johan Commelin, Josef Urban. Auto-hyperlinking the Stacks Project (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room)
• [WIP6] Deyan Ginev, Mihnea Iancu, Constantin Jucovshi, Andrea Kohlhase, Michael Kohlhase, Jürgen Schefter, Wolfram Sperber. The SMGloM Project and System (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room)
• [Poster1] Nathan Carter, Ken Monks. A web-based word processor with mathematical semantics (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room)
• [Poster2] Manfred Minimair. Math Chat in Collaborative Computer Algebra Shells (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room)
• [Poster3] Michael Kohlhase, Florian Rabe. The OAF Project: An Open Archive of Formalizations (Tuesday, 9:00-10:30 and 11:00-12:30, Meridian Room & Zenith Room)

Doctoral Programme

• [D1] Daniel Szymczak. Literate Development of Families of Mathematical Models (Monday, 9:00-9:45, Crescent Room)
• [D2] Dennis Müller. Knowledge Management across Formal Libraries (Monday, 9:45-10:30, Crescent Room)
• [D3] Daniel Selsam. Free and infinitely scalable advanced mathematics education (Monday, 11:00-11:45, Crescent Room)
• [D4] Waqar Ahmed. Formal Reliability Analysis using Higher-order Logic Theorem Proving (Monday, 11:45-12:30, Crescent Room)
• [D5] Discussion: How to give an effective presentation (Monday, 15:00-16:00, Crescent Room)
• [D6] Daniel Raggi. Change of representation in discrete mathematics (Monday, 16:30-17:15, Crescent Room)
• [D7] Individual discussions with mentors (Monday, 17:15-18:00, Crescent Room)

Workshop Mathematical User Interfaces (MathUI)

• [MA1] Davide Cervone, Peter Krautzberger, Volker Sorge. Towards Meaningful Visual Abstraction of Mathematical Notation (Monday, 9:45-10:30, Meridian Room)
• [MA2] Deyan Ginev, Nathan Jenkins,Alberto Pepe. Live Mathematics in Authorea: Data, Computation and Visualization (Monday, 11:00-11:45, Meridian Room)
• [MA3] Michael Kohlhase, Sourabh Lal, Tom Wiesing, Deyan Ginev. KAT: an Annotation Tool for STEM Documents (Monday, 11:45-12:30, Meridian Room)
• [MA4] Naomi Pentrel, Michael Kohlhase. Relational Presentation Using Semantic Closeness (Monday, 15:00-15:45, Meridian Room)
• [MA5] Philippe R. Richard, Michel Gagnon and Josep Maria Fortuny. Interactive management of problems in geometry for the development of student skills and the acquisition of mathematical knowledge (Monday, 16:30-17:15, Meridian Room)
• [MA6] Andrea Kohlhase and Ana Guseva:. Co-Occurrences of Context Dimensions of Spreadsheets (Monday, 17:15-18:00, Meridian Room)
• [MA7] Tool Demonstrations (Monday, 18:00-19:00, Meridian Room)

Workshop Formal Mathematics for Mathematicians (FM4M)

• [FM1] Cezary Kaliszyk. Invited talk: Learning to parse mathematics from aligned corpora (Wednesday, 9:05-9:50, Meridian Room)
• [FM2] Dennis Müller, Michael Kohlhase. Understanding Mathematical Theory Formation via Theory Intersections in MMT (Wednesday, 9:50-10:10, Meridian Room)
• [FM3] Marco Maggesi. A symbolic approach to abstract algebra in HOL Light (Wednesday, 10:10-10:30, Meridian Room)
• [FM4] Marco Maggesi. A formalisation of metric spaces in HOL Light (Wednesday, 11:00-11:20, Meridian Room)
• [FM5] Adam Naumowicz. Formalizing Divisibility Rules as a Student Case Study (Wednesday, 11:20-11:40, Meridian Room)
• [FM6] Mario Carneiro. GCH implies AC, a Metamath Formalization (Wednesday, 11:40-12:00, Meridian Room)
• [FM7] Karol Pąk. Improving Legibility of Proof Scripts in Mizar (Wednesday, 12:00-12:20, Meridian Room)
• [FM8] Closing discussion (Wednesday, 12:20-12:30, Meridian Room)

Workshop on computer Theorem proving components for Educational software (ThEdu)

• [TH1] Pedro Quaresma. Visual Geometry Proofs in a Learning Context (Wednesday, 9:00-9:30, Crescent Room)
• [TH2] Richard R. Philippe. Argumentative Effects of a Geometric Construction Tutorial System in Solving Problems of Proof (Wednesday, 9:30-10:00, Crescent Room)
• [TH3] Crispin Perdue. Creating Usable Computer Tools that Reason Mathematically (Wednesday, 10:00-10:30, Crescent Room)
• [TH4] Crispin Perdue. Mathtoys Demo (Wednesday, 11:00-12:00, Crescent Room)

Tutorials

• [T1] Tobias Nipkow. Isabelle Tutorial (Friday, 9:00-10:30 and 11:00-12:30, Meridian Room)

Social Events

• [S1] Lunch Banquet at Hill Country Barbecue Market DC (joint walk/travel, banquet starts 13:00) (Wednesday, 12:30/13:00-15:00, Hill Country Barbecue Market)
• [S2] Possibility to visit Smithsonian Museums (on your own) (Wednesday, 15:00-, Smithsonian Museums)

Business Meetings

• [B1] Business Meeting (Thursday, 17:30-18:30)