List of EventsInvited 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 GalloisWong, Sylvie Boldo and Thibault Hilaire. A Coq formalization of digital filters (Slides)
 [T2] Thierry DanaPicard and Zoltán Kovács. Automated determination of isoptics with dynamic geometry (Slides)
 [T3] Howard Cohl, André GreinerPetter 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. Proofofwork 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 HighPrecision 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. GoalOriented 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é GreinerPetter, 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: XSLbased 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 GalloisWong. Formal Verification and Digital Filters (Slides)
 [DP3] Philipp Scharpf. Formula Concept Discovery and Recognition
 [DP4] Andre GreinerPetter. 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 KoutsoukouArgyraki. Alexandria  Large Scale Formal Proof for the Working Mathematician
 [FMM2] Steffen Frerix and Peter Koepke. Automatic ProofChecking 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 wellwritten information about mathematical models and what can we do (Slides)
 [M3SRD2] Wolfram Sperber. The publicationbased 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 graphbased 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 MathintheMiddle 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? (CMEEI) [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 timetriggered hybrid systems, the platoon benchmark
 [FVPS3] P. Bhateja. A theoretical framework for testing cyberphysical systems
 [FVPS4] A. Rashid and O. Hasan. Formal modeling of robotic cell injection systems in higherorder 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
