List of Events

Invited Talks

[Invited Talk 1] Yves Bertot. A naive view of Homotopy Type Theory and its relation to the calculus of constructions (Monday, 11:30-12:30, Room (amphitheatre) Pedro Nunes (1st floor))
[Invited Talk 2] Jaime Carvalho e Silva. What international studies say about the importance and limitations of using computers to teach mathematics in secondary schools (Slides) (DOI) (Thursday, 11:30-12:30, Room (amphitheatre) Pedro Nunes (1st floor))
[Invited Talk 3] António Leal Duarte. Teaching Tiles (joint with ADG 2014) (Wednesday, 14:30-15:30, Amphitheatre of the Science Museum (Laboratorio Chimico))
[Invited Talk 4] Herbert Van de Sompel. Towards Robust Hyperlinks for Web-Based Scholarly Communication (DOI) (Friday, 11:30-12:30, Room (amphitheatre) Pedro Nunes (1st floor))
[Invited Talk 5] Eric Weisstein. Computable data, mathematics, and digital libraries in Mathematica and Wolfram|Alpha (DOI) (Tuesday, 11:30-12:30, Room (amphitheatre) Pedro Nunes (1st floor))

Regular papers

[R1] Waqar Ahmed, Osman Hasan, Sofiene Tahar and Mohamed Salah Hamdi. Formal Reliability Analysis of Oil and Gas Pipelines (DOI) (Tuesday, 14:30 - 15:00, Room (amphitheatre) Pedro Nunes (1st floor))
[R2] David Cerna. A Tableaux Based Decision Procedure for Multi-Parameter Propositional Schemata (Slides) (DOI) (Wednesday, 11:00 - 11:30, Room (amphitheatre) Pedro Nunes (1st floor))
[R3] Russell Bradford, Changbo Chen, James H. Davenport, Matthew England, Marc Moreno Maza and David Wilson. Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition (Slides) (DOI) (Tuesday, 10:30-11:00, Room (amphitheatre) Pedro Nunes (1st floor))
[R4] Andrew Fish and Alexei Lisitsa. Detecting unknots via equational reasoning, I: Exploration (DOI) (Tuesday, 15:00 - 15:30, Room (amphitheatre) Pedro Nunes (1st floor))
[R5] Zongyan Huang, Matthew England, David Wilson, James Davenport, Lawrence Paulson and James Bridge. Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition (Slides) (DOI) (Tuesday, 11:00-11:30, Room (amphitheatre) Pedro Nunes (1st floor))
[R6] Sanaz Khan-Afshar, Vincent Aravantinos, Osman Hasan and Sofiene Tahar. Formalization of Complex Vectors in Higher-Order Logic (DOI) (Wednesday, 12:00 - 12:30, Room (amphitheatre) Pedro Nunes (1st floor))
[R7] Moa Johansson, Dan Rosén, Nicholas Smallbone and Koen Claessen. Hipster: Integrating Theory Exploration in a Proof Assistant (Slides) (DOI) (Wednesday, 11:30 - 12:00, Room (amphitheatre) Pedro Nunes (1st floor))
[R8] Bernd Wegner and Sigram Schindler. Mathematical structures enabling the decidability of the patentability and patent eligibility of a patent application (DOI) (Tuesday, 15:30 - 16:00, Room (amphitheatre) Pedro Nunes (1st floor))
[R9] Andrea Kohlhase. Search Interfaces for Mathematicians (Slides) (DOI) (Friday, 9:30-10:00, Room (amphitheatre) Pedro Nunes (1st floor))
[R10] Michael Kohlhase. A Data Model and Encoding for a Semantic, Multilingual Glossary of Mathematics (DOI) (Friday, 9:00-9:30, Room (amphitheatre) Pedro Nunes (1st floor))
[R11] Ross Moore. PDF/A-3u as an archival format for Accessible mathematics (DOI) (Friday, 16:30-17:00, Room (amphitheatre) Pedro Nunes (1st floor))
[R12] Minh-Quoc Nghiem, Giovanni Yoko Kristianto, Goran Topic and Akiko Aizawa. Which one is better: presentation-based or content-based math search? (Slides) (DOI) (Friday, 11:00-11:30, Room (amphitheatre) Pedro Nunes (1st floor))
[R13] Ulf Schoeneberg and Wolfram Sperber. POS Tagging and its Applications for Mathematics (This paper has been awarded best DML paper prize) (Slides) (DOI) (Friday, 10:30-11:00, Room (amphitheatre) Pedro Nunes (1st floor))
[R14] Moritz Schubotz and Gabriel Wicke. Mathoid: Robust, Scalable, Fast and Accessible Math Rendering for Wikipedia (Slides) (DOI) (Friday, 16:00-16:30, Room (amphitheatre) Pedro Nunes (1st floor))
[R15] Marco B. Caminati, Manfred Kerber, Christoph Lange and Colin Rowat. Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle? (DOI) (Monday, 14:30-15:00, Room (amphitheatre) Pedro Nunes (1st floor))
[R16] Jacques Carette, William Farmer and Michael Kohlhase. Realms: A Structure for Consolidating Knowledge about Mathematical Theories (DOI) (Monday, 9:00 - 9:30, Room (amphitheatre) Pedro Nunes (1st floor))
[R17] Thomas Gransden, Neil Walkinshaw and Rajeev Raman. Mining State-Based Models from Proof Corpora (DOI) (Wednesday, 10:00-10:30, Room (amphitheatre) Pedro Nunes (1st floor))
[R18] Thibault Gauthier and Cezary Kaliszyk. Matching concepts across HOL libraries (DOI) (Monday, 10:30-11:00, Room (amphitheatre) Pedro Nunes (1st floor))
[R19] Yannis Haralambous and Pedro Quaresma. Querying Geometric Figures Using a Controlled Language, Ontological Graphs and Dependency Lattices (DOI) (Tuesday, 9:00-9:30, Room (amphitheatre) Pedro Nunes (1st floor))
[R20] Fulya Horozal, Michael Kohlhase and Florian Rabe. Flexary Operators for Formalized Mathematics (Slides) (DOI) (Monday, 15:00-15:30, Room (amphitheatre) Pedro Nunes (1st floor))
[R21] Lars Hupel. Interactive Simplifier Tracing and Debugging in Isabelle (Slides) (DOI) (Tuesday, 9:30-10:00, Room (amphitheatre) Pedro Nunes (1st floor))
[R22] Constantin Jucovschi. Towards an Interaction-based Integration of MKM Services into End-User Applications (DOI) (Wednesday, 9:30-10:00, Room (amphitheatre) Pedro Nunes (1st floor))
[R23] Cezary Kaliszyk and Florian Rabe. Towards Knowledge Management for HOL Light (Slides) (DOI) (Monday, 9:30 - 10:00, Room (amphitheatre) Pedro Nunes (1st floor))
[R24] Karol Pąk. Automated improving of proof legibility in the Mizar system (DOI) (Monday, 15:30-16:00, Room (amphitheatre) Pedro Nunes (1st floor))
[R25] Sana Stojanovic, Julien Narboux, Marc Bezem and Predrag Janicic. A Vernacular for Coherent Logic (DOI) (Monday, 11:00-11:30, Room (amphitheatre) Pedro Nunes (1st floor))
[R26] Qun Zhang and Abdou Youssef. Semantics-Sensitive Math-Similarity Search (DOI) (Wednesday, 9:00-9:30, Room (amphitheatre) Pedro Nunes (1st floor))
[R27] Howard Cohl, Marjorie McClain, Bonita Saunders, Moritz Schubotz and Janelle Williams. Digital Repository of Mathematical Formulae (DOI) (Friday, 16:30-18:00, Thursday 14:30-15:30, Thursday 16:00-18:00, Room 0.2 (0th floor))
[R28] Deyan Ginev and Joseph Corneli. NNexus Reloaded (DOI) (Friday, 16:30-18:00, Thursday 14:30-15:30, Thursday 16:00-18:00, Room 0.2 (0th floor))
[R29] Deyan Ginev, Bruce Miller and Silviu Oprea. E-books and Graphics with LaTeXML (DOI) (Friday, 16:30-18:00, Thursday 14:30-15:30, Thursday 16:00-18:00, Room 0.2 (0th floor))
[R30] Mihnea Iancu, Constantin Jucovschi, Michael Kohlhase and Tom Wiesing. System Description: MathHub.info (DOI) (Friday, 16:30-18:00, Thursday 14:30-15:30, Thursday 16:00-18:00, Room 0.2 (0th floor))
[R31] Cezary Kaliszyk, Josef Urban, Jiří Vyskočil and Herman Geuvers. Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description (DOI) (Friday, 16:30-18:00, Thursday 14:30-15:30, Thursday 16:00-18:00, Room 0.2 (0th floor))
[R32] Lukas Kohlhase and Michael Kohlhase. System Description: A Semantics-Aware LaTeX-to-Office Converter (DOI) (Friday, 16:30-18:00, Thursday 14:30-15:30, Thursday 16:00-18:00, Room 0.2 (0th floor))
[R33] Martin Líška, Petr Sojka and Michal Růžička. Math Indexer and Searcher Web Interface: Towards Fulfillment of Mathematiciansí Information Needs (Slides) (DOI) (Friday, 16:30-18:00, Thursday 14:30-15:30, Thursday 16:00-18:00, Room 0.2 (0th floor))
[R34] Adam Naumowicz. SAT-enhanced Mizar Proof Checking (DOI) (Friday, 16:30-18:00, Thursday 14:30-15:30, Thursday 16:00-18:00, Room 0.2 (0th floor))
[R35] Umair Siddique and Sofiene Tahar. A Framework for Formal Reasoning about Geometrical Optics (DOI) (Friday, 16:30-18:00, Thursday 14:30-15:30, Thursday 16:00-18:00, Room 0.2 (0th floor))

Work in progress

[W1] Hans-Gert Graebe, Andreas Nareike and Simon Johannig. The SymbolicData Project -- Towards a Computer Algebra Social Network (Monday, 16:30-17:00, Room (amphitheatre) Pedro Nunes (1st floor))
[W2] Robert Pagel and Moritz Schubotz. Mathematical Language Processing Project (Monday, 17:00-17:30, Room (amphitheatre) Pedro Nunes (1st floor))
[W3] Reinhard Kahle. Towards the Structure of Mathematical Proof (Monday, 17:30-18:00, Room (amphitheatre) Pedro Nunes (1st floor))
[W4] Jean-Guillaume Dumas, Dominique Duval, Burak Ekici and Jean-Claude Reynaud. Certified proofs in programs involving exceptions (Thursday, 9:00-9:30, Room (amphitheatre) Pedro Nunes (1st floor))
[W5] Washington de Carvalho Segundo, Flavio L. C. De Moura and Daniel Ventura. Formalizing a Named Explicit Substitutions Calculus in Coq (Thursday, 9:30-10:00, Room (amphitheatre) Pedro Nunes (1st floor))
[W6] Pedro Quaresma, Vanda Santos and Juan Moral. Reproducing a Geometric Working Session (Friday, 17:00-17:30, Room (amphitheatre) Pedro Nunes (1st floor))
[W7] Nils Schwinning, Melanie Schypula, Michael Striewe and Michael Goedicke. Concepts and realisations of flexible exercise design and feedbackgeneration in an e-assessment system for mathematics (Friday, 17:30-18:00, Room (amphitheatre) Pedro Nunes (1st floor))

Panel Discussions, Teaser Talks, Special Addresses, etc.

[P1] tentative list of panelists: Fabian Müller (FIZ/ZMath), Michael Kohlhase (Jacobs), [Herbert Van de Sompel (LANL)], Eric Weisstein (Wolfram|Aplha), Petr Sojka (Masaryk University). DML panel discussion: DMLs of Informal and Formal Mathematics: Marriage or Divorce? (Friday, 14:30 -- 15:30, Room (amphitheatre) Pedro Nunes (1st floor))
Abstract: There are two areas/worlds/directions where term DML (Digital Mathematics Libraries) is used: a) library of [informal] scientific [mostly peer-reviewed] papers that are have been written in the area of mathematics since Aristotle. Most papers in this world have been digitized and persistent pointers (DOIs, Zbl or MathSciNet IDs) are used as pointers to them. This allowed to build a web of linked and verified (reviews in referative databases) mathematical knowledge. In CICM jargon, DML track copes with this area and Herbert Van de Sompel's talk dealt with problems of linking and persistence in this world. b) library of [formal] mathematics knowledge, e.g. theorems formally proven by systems as Wolfram|Alpha, Coq, Mizar and others. Libraries of such math knowledge are poping up. In CICM jargon, MKM track copes with this area and Eric Weisstein's invited talk (eCF library) elaborated on current possibilities in this world.