List of Events

Invited Talks

• [I1] Akiko Aizawa. Natural language processing techniques for mathematical formula search (Slides)
• [I2] Bruno Buchberger. CICM, Calculemus, MKM, GMDL, ...: Some Thoughts About Past and Future (Slides)
• [I3] Adri Olde Daalhuis. The DLMF: special functions in the 21st century (Slides)

Calculemus

• [T1] Diane Gallois-Wong, Sylvie Boldo and Thibault Hilaire. A Coq formalization of digital filters (Slides)
• [T2] Thierry Dana-Picard and Zoltán Kovács. Automated determination of isoptics with dynamic geometry (Slides)
• [T3] Howard Cohl, André Greiner-Petter and Moritz Schubotz. Automated Symbolic and Numerical Testing of DLMF Formulae using a Computer Algebra System (Slides)
• [T4] Zoltán Kovács. Finding and proving new geometry theorems in regular polygons with dynamic geometry and automated reasoning tools (Slides)
• [T5] Alexander Maletzky and Fabian Immler. Groebner Bases of Modules and Faugere's F4 Algorithm in Isabelle/HOL (Slides)
• [T6] William Farmer, Jacques Carette and Yasmine Sharoda. Biform Theories: Project Description (Slides)
• [T30] Erich Kaltofen. Proof-of-work Certificates for High Complexity Mathematical Computations

Digital Mathematical Libraries

• [T7] Andrea Kohlhase, Michael Kohlhase and Taweechai Ouypornkochagorn. Discourse Phenomena in Math Documents (Slides)

Mathematical Knowledge Management

• [T8] Dennis Müller, Michael Kohlhase and Florian Rabe. Automatically Finding Theory Morphisms for Knowledge Management (Slides)
• [T9] Qingxiang Wang, Cezary Kaliszyk and Josef Urban. First Experiments with Neural Translation of Informal to Formal Mathematics (Slides)
• [T10] Cezary Kaliszyk and Karol Pąk. Isabelle Import Infrastructure for the Mizar Mathematical Library (Slides)
• [T11] Theresa Pollinger, Michael Kohlhase and Harald Köstler. Knowledge Amalgamation for Computational Science and Engineering (Slides)
• [T12] Manfred Minimair. Model and Software System MathChat: Computational Mathematics with Collaborative Chat
• [T13] Jonas Betzendahl and Michael Kohlhase. Translating the IMPS Theory Library to MMT/OMDoc (Slides)
• [T14] Achim Brucker, Paolo Crisafulli, Idir Ait Sadoune and Burkhart Wolff. Using The Isabelle Ontology Framework: Linking the Formal with the Informal (Slides)
• [T15] Abdou Youssef and Bruce Miller. Deep Learning for Math Knowledge Processing (Slides)
• [T27] Alberto Fiori and Claudio Sacerdoti Coen. Towards an implementation in LambdaProlog of the two level Minimalist Foundation (Slides)
• [T28] Jan Frederik Schaefer and Michael Kohlhase. Syntactic/Semantic Analysis for High-Precision Math Linguistics (Slides)
• [T29] Felix Petersen, Moritz Schubotz and Bela Gipp. Towards Formula Translation using Recursive Neural Networks (Slides)

Systems and Demos

• [T16] Łukasz Czajka, Burak Ekici and Cezary Kaliszyk. Concrete Semantics with Coq and CoqHammer (Slides)
• [T17] Yutaka Nagashima and Julian Parsert. Goal-Oriented Conjecturing for Isabelle/HOL (Slides)
• [T18] Wolfgang Schreiner. Validating Mathematical Theorems and Algorithms with RISCAL (Slides)
• [T19] Jan Jakubuv and Josef Urban. Enhancing ENIGMA Given Clause Guidance (Slides)
• [T20] Andreas Humenberger, Maximilian Jaroschek and Laura Kovacs. Aligator.jl — A Julia Package for Loop Invariant Generation (Slides)
• [T21] Michael Junk, Stefan Hölle and Sebastian Sahli. Formalized Mathematical Content in Lecture Notes on Modelling and Analysis (Slides)
• [T22] André Greiner-Petter, Moritz Schubotz, Howard Cohl and Bela Gipp. MathTools: An Open API for Convenient MathML Handling (Slides)
• [T23] Grzegorz Bancerek, Adam Naumowicz and Josef Urban. System Description: XSL-based Translator of Mizar to LaTeX (Slides)
• [T24] Moritz Schubotz. VMEXT2: A Visual Wikidata aware Content MathML Editor (Slides)
• [T25] Richard Marcus, Michael Kohlhase and Florian Rabe. Demo: TGView3D for Immersive Theory Graph Exploration (Slides)
• [T26] Michael Kohlhase. Demo: Math Object Identifiers -- Towards Research Data in Mathematics (Slides)

Doctoral Programme

• [DP1] Jonas Betzendahl. Formal Languages for Mathematics (Slides)
• [DP2] Diane Gallois-Wong. Formal Verification and Digital Filters (Slides)
• [DP3] Philipp Scharpf. Formula Concept Discovery and Recognition
• [DP4] Andre Greiner-Petter. Automatic Mathematical Information Retrieval to perform translations up to Computer Algebra Systems (Slides)
• [DP5] Discussion

Special Session

• [S1] Bruce Miller (nominated by Michael Kohlhase). News on LaTeXML
• [S2] Moritz Schubotz. Open Science in CICM
• [S3] Michael Kohlhase. News on MathML
• [S4] Florian Rabe. AI for CICM
• [S5] Bill Farmer. The Future of CICM (skipped)
• [S6] Felix Petersen. LaTeXEqChecker - A framework for checking mathematical semantics in LaTeX documents (Slides)

Business Meeting

• [BM1] Bill Farmer. Steering Committee Report (Slides)
• [BM2] Jan Jakubuv. CICM 2019 Preview
• [BM3] Wolfgang Windsteiger. Conference Chair Report
• [BM4] Florian Rabe. Program Chair Report (Slides)

Workshop on Formal Mathematics for Mathematicians (FMM)

• [FMM1] Angeliki Koutsoukou-Argyraki. Alexandria - Large Scale Formal Proof for the Working Mathematician
• [FMM2] Steffen Frerix and Peter Koepke. Automatic Proof-Checking of Ordinary Mathematical Texts
• [FMM3] Michael Junk, Sebastian Sahli and Stefan Hölle. A Meta Language for Mathematical Reasoning
• [FMM4] Karol Pąk. Progress in the Formalization of Matiyasevich's theorem in the Mizar system (Slides)
• [FMM5] Burak Ekici. Towards Mac Lane's Comparison Theorem for the (co)Kleisli construction in Coq (Slides)
• [FMM6] Slawomir Kolodynski. IsarMathLib - a formalized mathematics library for Isabelle/ZF (Slides)

Workshop on Mathematical Models and Mathematical Software as Research Data (M3SRD)

• [M3SRD1] Michael Kohlhase. Mathematical model as research data - why do need precise and well-written information about mathematical models and what can we do (Slides)
• [M3SRD2] Wolfram Sperber. The publication-based approach for mathematical models: Identification of mathematical models in the literature and processing of information about mathematical models from publications (Slides)
• [M3SRD3] Thomas Koprucki. A graph-based representation of mathematical modeling and models
• [M3SRD4] Florian Rabe. A concept for the formalization of mathematical models

OpenMath Workshop

• [OpMa1] Moritz Schubotz. Representing Mathematical Formulae in Content MathML using Wikidata (Slides)
• [OpMa2] Tom Wiesing and Michael Kohlhase. OpenMath in JSON (Slides)
• [OpMa3] Bruce Miller. A new SpecFun Content Dictionary (Slides)
• [OpMa4] OpenMath Society. OpenMath Society Business Meeting (Slides)

Workshop on Computer Algebra in the Age of Types (CAAT)

• [CAAT1] Michael Kohlhase. Keynote: Composing Mathematical Software Systems via the Math-in-the-Middle Paradigm (Slides)
• [CAAT2] Sebastian Gutsche, Sebastian Posur, Øystein Skartsæterhagen. Categories, Algorithms, and Programming
• [CAAT3] Edwin Brady. Idris Tutorial
• [CAAT4] Dennis Müller. The MMT System
• [CAAT5] Discussion. Prototyping and development with Idris, MMT, and other tools

Workshop on Computer Mathematics in Education --- Enlightenment or Incantation? (CME-EI)

• [CMEEI1] Christopher Sangwin. Sangwin - High stakes automatic assessments: developing an online linear algebra examination (Slides)
• [CMEEI2] Zoltan Kovacs. Advantages and dangers on utilizing GeoGebra Automated Reasoning Tools (Slides)
• [CMEEI3] Wolfgang Schreiner. Logic as a Path to Enlightenment (Work in Progress Report) (Slides)
• [CMEEI4] Walther Neuper. Mechanical Explanation in "Systems that Explain Themselves" (Slides)
• [CMEEI5] Franz Lichtenberger. Intelligent Computer Mathematics OR Mathematics for Intelligent Computing? (Slides)

Workshop on Formal Verification of Physical Systems (FVPS)

• [FVPS1] S. Tahar, O. Hasan and U. Siddique. Formal verification of cyber physical systems – a survey
• [FVPS2] F. Bidet, E. Goubault and S. Putot. Work in progress: reachability analysis for time-triggered hybrid systems, the platoon benchmark
• [FVPS3] P. Bhateja. A theoretical framework for testing cyber-physical systems
• [FVPS4] A. Rashid and O. Hasan. Formal modeling of robotic cell injection systems in higher-order logic
• [FVPS5] H. Zaatiti, L. Ye, P. Dague and J.P. Gallois. Automating abstraction computation of hybrid systems
• [FVPS6] Discussion. Towards Formal Frameworks for Modeling, Simulation, and Verification of Physical Systems