List of Events

Invited Talks

• [I0] Ursula Martin and Alison Pease. Mathematical practice, crowdsourcing, and social machines (DOI) (Thursday, 9:00-10:00, Room 8W 2.1)
• [I1] Assia Mahboubi. A Machine-checked proof of the Odd Order Theorem (DOI) (Monday, 11:30-12:30, Room 8W 2.1)
• [I2] Patrick Ion. Mathematics and the World Wide Web (DOI) (Friday, 9:00-10:00, Room 8W 2.1)
• [R500] Conor McBride. Problems as Types (Tuesday, 10:30-11:30, Room 8W 2.1)
• [R501] Sergei Meshveliani. Dependent Types for an Adequate Programming of Algebra (Tuesday, 11:30-12:30, Room 8W 2.1)
• [R502] Edwin Brady. Dependently Typed Functional Programming in Idris (Tuesday, 14:00-15:00, Room 8W 2.1)
• [R504] Gilles Dowek. Checking classical proofs in a constructive proof-checker (Tuesday, 16:00-17:00, Room 8W 2.1)

Regular papers

• [R1] Russell Bradford, James H. Davenport, Matthew England and David Wilson. Optimising Problem Formulation for Cylindrical Algebraic Decomposition (DOI) (Monday, 14:00-14:30, Room 8W 2.1)
• [R2] William Farmer. The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and Evaluation (DOI) (Monday, 16:00-16:30, Room 8W 2.1)
• [R3] Xavier Allamigeon, Stéphane Gaubert, Victor Magron and Benjamin Werner. Certification of Bounds of Non-linear Functions: the Templates Method (DOI) (Monday, 14:30-15:00, Room 8W 2.1)
• [R4] Jónathan Heras, Gadea Mata, Ana Romero, Julio Rubio and Rubén Sáenz. Verifying a platform for digital imaging: a multi-tool strategy (DOI) (Monday, 15:00-15:30, Room 8W 2.1)
• [R5] Michael Kohlhase, Felix Mance and Florian Rabe. A Universal Machine for Biform Theory Graphs (DOI) (Monday, 16:30-17:00, Room 8W 2.1)
• [R6] Christoph Lüth and Martin Ring. A Web Interface for Isabelle: The Next Generation (Slides) (DOI) (Tuesday, 09:40-09:45,10:30-12:30,14:00-15:30,16:00-18:00, Room 8W 2.30)
• [R7] Christoph Lange, Colin Rowat and Manfred Kerber. The ForMaRE Project – Formal Mathematical Reasoning in Economics (Slides) (DOI) (Tuesday, 09:55-10:00,10:30-12:30,16:00-18:00, Room 8W 2.30)
• [R8] Deyan Ginev and Bruce Miller. LaTeXML 2012 - A Year of LaTeXML (Slides) (DOI) (Tuesday, 09:15-09:20,presentation times to be confirmed, Room 8W 2.30)
• [R9] Florian Rabe. The MMT API: A Generic MKM System (DOI) (Tuesday, 09:35-09:40,presentation times to be confirmed, Room 8W 2.30)
• [R10] Dmitry Chebukov, Alexandr Izaak, Olga Misurina, Yury Pupyrev and Alexey Zhizhchenko. Math-Net.Ru as a Digital Archive of the Russian Mathematical Knowledge from the XIX Century to Today (Slides) (DOI) (Tuesday, 09:05-09:10,10:30-12:30,14:00-15:30,16:00-18:00, Room 8W 2.30)
• [R11] Miguel A. Abanades and Francisco Botana. A dynamic symbolic geometry environment based on the GröbnerCover algorithm for the computation of geometric loci and envelopes (Slides) (DOI) (Tuesday, 09:00-09:05,10:30-12:30,14:00-15:30, Room 8W 2.30)
• [R12] Jónathan Heras and Ekaterina Komendantskaya. ML4PG in Computer Algebra verification (Slides) (DOI) (Tuesday, 09:45-09:50,10:30-12:30,14:00-15:30,16:00-18:00, Room 8W 2.30)
• [R13] Bruno Barras, Hugo Herbelin, Lourdes Del Carmen González Huesca, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel and Burkhart Wolff. Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems (Slides) (DOI) (Tuesday, 09:50-09:55,10:30-12:30,14:00-15:30,16:00-17:30, Room 8W 2.30)
• [R14] Pedro Quaresma, Vanda Santos and Seifeddine Bouallegue. The Web Geometry Laboratory Project (Slides) (DOI) (Tuesday, 09:25-09:30,10:30-12:30,14:00-15:30, Room 8W 2.30)
• [R15] Sebastian Bönisch, Michael Brickenstein, Hagen Chrapary, Gert-Martin Greuel and Wolfram Sperber. swMATH - a new service for mathematics software (Slides) (DOI) (Tuesday, 09:20-09:25,10:30-12:30,14:00-15:30,16:00-18:00, Room 8W 2.30)
• [R16] Rein Prank. Software for evaluating relevance of steps in algebraic transformations (Slides) (DOI) (Tuesday, 09:30-09:35,11:30-12:30,14:00-15:30,16:00-18:00, Room 8W 2.30)
• [R17] Ulf Schöneberg and Wolfram Sperber. Text analysis in mathematics - the DeLiVerMATH project (Slides) (DOI) (Tuesday, 09:10-09:15,10:30-12:00,14:30-15:30,16:00-17:00, Room 8W 2.30)
• [R18] Shahab Kamali and Frank Tompa. Structural Similarity Search For Mathematics Retrieval (DOI) (Thursday, 10:30-11:00, Room 8W 2.1)
• [R19] Michal Růžička, Petr Sojka and Vlastimil Krejčíř. Towards Machine-Actionable Modules of a Digital Mathematics Library (Slides) (DOI) (Thursday, 15:00-15:30, Room 8W 2.1)
• [R20] Minh-Quoc Nghiem, Giovanni Yoko Kristianto, Goran Topic and Akiko Aizawa. A hybrid approach for semantic enrichment of MathML mathematical expressions (DOI) (Thursday, 11:00-11:30, Room 8W 2.1)
• [R21] Bruce Miller. 3 Years of DLMF on the Web; Math & Search (DOI) (Thursday, 11:30-12:00, Room 8W 2.1)
• [R22] Paul Libbrecht. Escaping the Trap of too Precise Topic Queries (Slides) (DOI) (Thursday, 14:00-14:30, Room 8W 2.1)
• [R23] Chau Do and Eric Pauwels. Using MathML to Represent Units of Measurement for Improved Ontology Alignment (DOI) (Thursday, 14:30-15:00, Room 8W 2.1)
• [R24] Cezary Kaliszyk and Josef Urban. Automated Reasoning Service for HOL Light (DOI) (Friday, 10:30-11:00, Room 8W 2.1)
• [R25] Matthew England, Russell Bradford, James H. Davenport and David Wilson. Understanding branch cuts of expressions (DOI) (Thursday, 16:30-17:00, Room 8W 2.1)
• [R26] Carst Tankink, Cezary Kaliszyk, Josef Urban and Herman Geuvers. Formal Mathematics on Display: A Wiki for Flyspeck (DOI) (Friday, 11:30-12:00, Room 8W 2.1)
• [R27] Rui Hu and Stephen Watt. Determining Points on Handwritten Mathematical Symbols (DOI) (Thursday, 16:00-16:30, Room 8W 2.1)
• [R28] Steven Obua, Mark Adams and David Aspinall. Capturing Hiproofs in HOL Light (DOI) (Friday, 11:00-11:30, Room 8W 2.1)
• [R29] Christoph Lange, Marco Caminati, Manfred Kerber, Till Mossakowski, Colin Rowat, Makarius Wenzel and Wolfgang Windsteiger. A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory (Slides) (DOI) (Thursday, 17:30-18:00, Room 8W 2.1)
• [R30] Eno Tonisson. Students' Comparison of Their Trigonometric Answers with the Answers of a Computer Algebra System (DOI) (Thursday, 17:00-17:30, Room 8W 2.1)

Work in progress

• [R200] Ross Moore. Tagged Mathematics in PDFs for Accessibility and other purposes (Tuesday, 10:30-11:00, Room 8W 2.27)
• [R201] Jozef Mišutka. Scaling Feature Based Mathematical Search Engine for Real-World Document Sets (Tuesday, 11:00-11:30, Room 8W 2.27)
• [R202] Dave Murray-Rust and Peter Murray-Rust. The Declaratron, semantic specification for scientific computation using MathML (Tuesday, 11:30-12:00, Room 8W 2.27)
• [R203] Nathan Carter and Kenneth Monks. Lurch: A Word Processor that Can Grade Students' Proofs (Tuesday, 12:00-12:30, Room 8W 2.27)
• [R204] Demos of systems R200, R201, R202, R203 (Tuesday, 14:00-15:30,16:00-17:30, Room 8W 2.27)

Panel Discussions, Teaser Talks, Special Addresses, etc.

• [B4] Thierry Bouche (EuDML), Patrick Ion (MR), Wolfram Sperber (ZBMath). DML Panel discussion: Fifty Shades of *DML (Wednesday, 18:00-19:00, Room 8W 2.1)

  Abstract: There are continuation efforts ongoing with the dream of WDML in mind: EuDML has finished its initial phase, so as preparatory project granted by Sloan foundation, and there are other DML projects maturing (RusDML, Euclid, CEDRAM, etc.) Views on who and how to proceed differ. Some decisions were discussed at DML panel last year. It is time now to stop for a while, and ask for feedback from the community. aa) Have running projects as EuDML, Euclid or preparatory WDML (Sloan) met community expectations? ab) What are pros and cons? ac) Which services are good and which are lacking? ba) How DMLs relate to the established services as MR and ZMath? bb) Do they complement their service? bc) What are the prospects of their future interactions? c) What is the current view of WDML services and how should sustainability and curation be secured by the community, if any?

• [T1] Teaser talks for posters/demos R11, R10, R17, R8, R15, R14, R9, R6, R12, R13, R7 (Slides) (Tuesday, 09:00-10:00, Room 8W 2.1)

Workshop Mathematical User Interfaces (MathUI)

• [R300] Jan Wilken Doerrie and Michael Kohlhase. MathMap: Accessing Math via Interactive Maps (Wednesday, 08:30-09:00, Room 8W 2.1)
• [R301] Jan Willem Knopper and Hans Cuypers. Interactive Mathematical Videos (Wednesday, 16:00-16:30, Room 8W 2.1)
• [R302] Deyan Ginev. NNexus Glasses: A Drop-in Showcase for Wikification (Wednesday, 15:00-15:30, Room 8W 2.1)
• [R303] Eric Andres, Bastiaan Heeren and Johan Jeuring. Towards Automatic Generation of Domain-Specific Mathematical Input Support (Wednesday, 10:30-11:00, Room 8W 2.1)
• [R304] Anjo Anjewierden, Ellen T. Kamp and Ton de Jong. Ziggy: Very Interactive Trigonometry (Wednesday, 11:00-11:30, Room 8W 2.1)
• [R305] Jean-François Nicaud and Christophe Viudez. Implementation of Dynamic Algebra in Epsilonwriter (Wednesday, 11:30-12:00, Room 8W 2.1)
• [R306] Rui Hu and Stephen Watt. InkChat: A Collaboration Tool for Mathematics (Wednesday, 12:00-12:30, Room 8W 2.1)
• [R307] Vadim Mazalov and Stephen Watt. Recommendation Systems in Mathematical Character Recognition (Wednesday, 14:00-14:30, Room 8W 2.1)
• [R308] Daniel Marques. Edition with Arabic mathematical notation (Wednesday, 14:30-15:00, Room 8W 2.1)
• [R309] Mihnea Iancu, Felix Mance and Florian Rabe. The Scala-REPL + MMT as a Lightweight Mathematical User Interface (Wednesday, 09:30-10:00, Room 8W 2.1)
• [R310] Andrea Kohlhase. Spreadsheets: From Data Interfaces to Knowledge Interfaces (Wednesday, 09:00-09:30, Room 8W 2.1)

OpenMath Workshop

• [R100] Lars Hellström. Literate Sources for Content Dictionaries (Wednesday, 09:00-09:30, Room 8W 2.27)
• [R101] Nathan Carter and Kenneth Monks. Lurch: A Word Processor Built on OpenMath that Can Check Mathematical Reasoning (Wednesday, 09:30-10:00, Room 8W 2.27)
• [R102] Lars Hellström. Quantifiers and n-ary Binders: an OpenMath Standard Enhancement Proposal (Wednesday, 10:30-11:00, Room 8W 2.27)

Programming Languages for Mechanized Mathematics Systems Workshop (PLMMS)

• [R503] Nicola Botta, Cezar Ionescu and Edwin Brady. Sequential decision problems, dependently-typed solutions (Tuesday, 15:00-15:30, Room 8W 2.1)
• [R505] Clemens Ballarin. Reading an Algebra Textbook (Tuesday, 17:00-17:30, Room 8W 2.1)

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

• [R600] Nuno Baeta and Pedro Quaresma. The Full Angle Method on the OpenGeoProver (Wednesday, 14:00-14:30, Room 8W 2.28)
• [R601] Walter Neuper. Computer Algebra implemented in Isabelle's Function Package under Lucas-Interpretation - a Case Study (Wednesday, 14:30-15:00, Room 8W 2.28)

Doctoral Programme

• [D1] David Wilson. Advances in Cylindrical Algebraic Decomposition (Wednesday, 14:00-14:30, Room 8W 2.27)
• [D2] Minh-Quoc NGHIEM. Semantic enrichment for mathematical expressions and its application to math search problem (Wednesday, 14:30-15:00, Room 8W 2.27)
• [D3] Michal Růžička. Maths Information Retrieval for Digital Libraries (Wednesday, 15:00-15:30, Room 8W 2.27)
• [D4] Ieuan Evans. Machine Learning Techniques Applied to Mathematical Formulae Recognition (Wednesday, 16:00-16:30, Room 8W 2.27)
• [D5] Behrang S. Saroui. Offline Segmentation and Recognition of Handwritten Mathematical Notes on Whiteboards (Wednesday, 16:30-17:00, Room 8W 2.27)
• [D6] Rui Hu. Pen-Based Collaboration Tools for Mathematics (Wednesday, 17:00-17:30, Room 8W 2.27)
• [D7] Mihnea Iancu. Towards Flexiformal Mathematics (Wednesday, 17:30-18:00, Room 8W 2.27)

Business Meetings

• [B0] Calculemus. Business meeting (Monday, 17:15-18:00, Room 8W 2.1)
• [B1] MKM. Business meeting (Thursday, 18:10-18:50)
• [B2] CICM. CICM Business meeting (Tuesday, 18:00-18:30)
• [B3] DML. Business meeting (Wednesday, 19:00-19:20, Room 8W 2.1)
• [B5] OpenMath. Business meeting (Wednesday, 11:00-11:45, Room 8W 2.27)

Social Events

• [S1] Banquet (Tuesday, )