List of EventsInvited Talks [Invited Talk Jim Pitman] Jim Pitman. Towards a Global Digital Mathematics Library (Monday, 14:0015:00, Meridian Room)
 [Invited Talk Richard Zanibbi] Richard Zanibbi (with Awelemdy Orakwue). Math Search for the Masses: Multimodal Search Interfaces and AppearanceBased Retrieval (DOI) (Tuesday, 14:0015: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:0015:00, Meridian Room)
 [Invited Talk Leonardo de Moura] Leonardo de Moura. Formalizing mathematics using the Lean Theorem Prover (DOI) (Friday, 14:0015:00, Meridian Room)
Calculemus [R1] Waqar Ahmed and Osman Hasan. Towards Formal Fault Tree Analysis using Theorem Proving (DOI) (Thursday, 15:0015:30, Meridian Room)
 [R2] Luís CruzFilipe and Peter SchneiderKamp. Optimizing a Certified Proof Checker for a LargeScale ComputerGenerated Proof (DOI) (Thursday, 15:3016:00, Meridian Room)
 [R3] Evgenii Kotelnikov, Laura Kovacs and Andrei Voronkov. A First Class Boolean Sort in FirstOrder Theorem Proving and TPTP (DOI) (Thursday, 16:3017:00, Meridian Room)
 [R4] Steven Obua, Jacques Fleuriot, Phil Scott and David Aspinall. Type Inference for ZFH (DOI) (Thursday, 17:0017:30, Meridian Room)
 [R5] Florian Rabe. Generic Literals (DOI) (Friday, 15:0015:30, Meridian Room)
 [R6] Paul Tarau. Ranking/unranking of Lambda Terms with Compressed de Bruijn Indices (DOI) (Friday, 15:3016:00, Meridian Room)
Digital Mathematical LibrariesMathematical Knowledge Management [R8] Serge Autexier and Dieter Hutter. Structure Formation in Large Theories (DOI) (Tuesday, 15:3016:00, Meridian Room)
 [R9] Fulya Horozal and Florian Rabe. Formal Logic Definitions for Interchange Languages (DOI) (Tuesday, 16:3017:00, Meridian Room)
 [R10] Mihnea Iancu and Michael Kohlhase. Math Literate Knowledge Management via Induced Material (DOI) (Tuesday, 17:0017:30, Meridian Room)
 [R11] Bruce Miller. Strategies for Parallel Markup (DOI) (Tuesday, 17:3018:00, Meridian Room)
 [R12] Karol Pąk. Readable Formalization of Euler's Partition Theorem in Mizar (DOI) (Thursday, 11:0011: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:3012:00, Meridian Room)
 [R14] Qun Zhang and Abdou Youssef. Performance Evaluation and Optimization of MathSimilarity Search (DOI) (Thursday, 12:0012:30, Meridian Room)
Projects & Surveys [R17] Cezary Kaliszyk, Josef Urban, Umair Siddique, Sanaz KhanAfshar, Cvetan Dunchev and Sofiene Tahar. Formalizing Physics: Automation, Presentation and Foundation Issues (DOI) (Tuesday, 9:0010:30 and 11:0012:30, Meridian Room & Zenith Room)
 [R19] Umair Siddique, Osman Hasan and Sofiene Tahar. Towards the Formalization of Fractional Calculus in Higherorder Logic (DOI) (Tuesday, 9:0010:30 and 11:0012:30, Meridian Room & Zenith Room)
 [R20] Max Wisniewski, Alexander Steen and Christoph Benzmüller. LeoPARD  A Generic Platform for the Implementation of HigherOrder Reasoners (DOI) (Tuesday, 9:0010:30 and 11:0012: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: Stateoftheart and Beyond (DOI) (Thursday, 9:009:45, Meridian Room)
 [R18] Claudio Sacerdoti Coen and Ferruccio Guidi. A Survey on Retrieval of Mathematical Knowledge (DOI) (Thursday, 9:4510: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:3018:00, Meridian Room)
Systems & Data [R21] Moa Johansson, Dan Rosén, Nicholas Smallbone and Koen Claessen. TIP: Tons of Inductive Problems (DOI) (Tuesday, 9:0010:30 and 11:0012:30, Meridian Room & Zenith Room)
 [R22] Ross Moore. Semantic Enrichment of Mathematics via `tooltips' (DOI) (Tuesday, 9:0010:30 and 11:0012:30, Meridian Room & Zenith Room)
 [R23] Kazuhisa Nakasho and Yasunari Shidama. Documentation Generator Focusing on Symbols for the HTMLized Mizar Library (DOI) (Tuesday, 9:0010:30 and 11:0012:30, Meridian Room & Zenith Room)
 [R24] Adam Naumowicz. Tools for MML Environment Analysis (DOI) (Tuesday, 9:0010:30 and 11:0012:30, Meridian Room & Zenith Room)
 [R25] Ons Seddiki, Cvetan Dunchev, Sanaz KhanAfshar and Sofiene Tahar. Enabling Symbolic and Numerical Computations in HOL Light (DOI) (Tuesday, 9:0010:30 and 11:0012:30, Meridian Room & Zenith Room)
Work in progress [WIP1] Bob Neveln, Bob Alps. Parsing Texts and Checking Proofs in LaTeX (Friday, 16:3017:00, Meridian Room)
 [WIP2] Mario Carneiro. Arithmetic in Metamath, Case Study: Bertrand's Postulate (Friday, 17:0017:30, Meridian Room)
 [WIP3] Théo Zimmermann, Hugo Herbelin. Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant (Tuesday, 18:0018:30, Meridian Room)
 [WIP4] Pedro Quaresma, Vanda Santos, Milena Marić. A Web Environment for Geometry (Tuesday, 9:0010:30 and 11:0012:30, Meridian Room & Zenith Room)
 [WIP5] Johan Commelin, Josef Urban. Autohyperlinking the Stacks Project (Tuesday, 9:0010:30 and 11:0012: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:0010:30 and 11:0012:30, Meridian Room & Zenith Room)
 [Poster1] Nathan Carter, Ken Monks. A webbased word processor with mathematical semantics (Tuesday, 9:0010:30 and 11:0012:30, Meridian Room & Zenith Room)
 [Poster2] Manfred Minimair. Math Chat in Collaborative Computer Algebra Shells (Tuesday, 9:0010:30 and 11:0012:30, Meridian Room & Zenith Room)
 [Poster3] Michael Kohlhase, Florian Rabe. The OAF Project: An Open Archive of Formalizations (Tuesday, 9:0010:30 and 11:0012:30, Meridian Room & Zenith Room)
Doctoral Programme [D1] Daniel Szymczak. Literate Development of Families of Mathematical Models (Monday, 9:009:45, Crescent Room)
 [D2] Dennis Müller. Knowledge Management across Formal Libraries (Monday, 9:4510:30, Crescent Room)
 [D3] Daniel Selsam. Free and infinitely scalable advanced mathematics education (Monday, 11:0011:45, Crescent Room)
 [D4] Waqar Ahmed. Formal Reliability Analysis using Higherorder Logic Theorem Proving (Monday, 11:4512:30, Crescent Room)
 [D5] Discussion: How to give an effective presentation (Monday, 15:0016:00, Crescent Room)
 [D6] Daniel Raggi. Change of representation in discrete mathematics (Monday, 16:3017:15, Crescent Room)
 [D7] Individual discussions with mentors (Monday, 17:1518:00, Crescent Room)
Workshop Mathematical User Interfaces (MathUI) [MA1] Davide Cervone, Peter Krautzberger, Volker Sorge. Towards Meaningful Visual Abstraction of Mathematical Notation (Monday, 9:4510:30, Meridian Room)
 [MA2] Deyan Ginev, Nathan Jenkins,Alberto Pepe. Live Mathematics in Authorea: Data, Computation and Visualization (Monday, 11:0011:45, Meridian Room)
 [MA3] Michael Kohlhase, Sourabh Lal, Tom Wiesing, Deyan Ginev. KAT: an Annotation Tool for STEM Documents (Monday, 11:4512:30, Meridian Room)
 [MA4] Naomi Pentrel, Michael Kohlhase. Relational Presentation Using Semantic Closeness (Monday, 15:0015: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:3017:15, Meridian Room)
 [MA6] Andrea Kohlhase and Ana Guseva:. CoOccurrences of Context Dimensions of Spreadsheets (Monday, 17:1518:00, Meridian Room)
 [MA7] Tool Demonstrations (Monday, 18:0019:00, Meridian Room)
Workshop Formal Mathematics for Mathematicians (FM4M) [FM1] Cezary Kaliszyk. Invited talk: Learning to parse mathematics from aligned corpora (Wednesday, 9:059:50, Meridian Room)
 [FM2] Dennis Müller, Michael Kohlhase. Understanding Mathematical Theory Formation via Theory Intersections in MMT (Wednesday, 9:5010:10, Meridian Room)
 [FM3] Marco Maggesi. A symbolic approach to abstract algebra in HOL Light (Wednesday, 10:1010:30, Meridian Room)
 [FM4] Marco Maggesi. A formalisation of metric spaces in HOL Light (Wednesday, 11:0011:20, Meridian Room)
 [FM5] Adam Naumowicz. Formalizing Divisibility Rules as a Student Case Study (Wednesday, 11:2011:40, Meridian Room)
 [FM6] Mario Carneiro. GCH implies AC, a Metamath Formalization (Wednesday, 11:4012:00, Meridian Room)
 [FM7] Karol Pąk. Improving Legibility of Proof Scripts in Mizar (Wednesday, 12:0012:20, Meridian Room)
 [FM8] Closing discussion (Wednesday, 12:2012:30, Meridian Room)
Workshop on computer Theorem proving components for Educational software (ThEdu)TutorialsSocial EventsBusiness Meetings
