You must enable JavaScript to use this site
  • 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)


    • [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
  • News

    • CICM is over
    • award winners online
    • detailed program online
    • accepted papers online
    • registration open
    • program overview online
    • deadline extended: April 22 (abstract), April 29 (paper)
    • 6 workshops accepted
    • 3 invited speakers
    • CfP and CfW available
    • PC completed
    • initial website online
Privacy policy and legal information
Last modified: October 12 2018 15:03:45 CEST