You must enable JavaScript to use this site
  • List of Events

    Invited Talks

    • [I1] Alan Bundy. Reformation: A Generic Algorithm for Repairing Faulty Logical Theories
    • [I2] Przemyslaw Chojecki. DeepAlgebra - an outline of a program
    • [I3] Grant Passmore. Formal Verification of Financial Algorithms, Progress and Prospects


    • [C1] William Farmer and Jacques Carette. Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study
    • [C2] Alexander Maletzky and Wolfgang Windsteiger. The Formalization ofVickrey Auctions: A Comparison of Two Approaches in Isabelle and Theorema
    • [C3] Franck Slama and Edwin Brady. Automatically Proving Equivalence by Type-Safe Reflection

    Digital Mathematical Libraries

    • [D1] Patrick Ion and Stephen Watt. The Global Digital Mathematics Library and The International Mathematical Knowledge Trust
    • [D2] Olivier Labbe and Thierry Bouche. The New Numdam platform
    • [D3] Dennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase and Florian Rabe. Classification of Alignments between Concepts of Formal Mathematical Systems
    • [D4] Wolfram Sperber and Michael Kohlhase. Software Citations, swMATH, and Beyond

    Mathematical Knowledge Management

    • [M1] Marco B. Caminati and Juliana Küster Filipe Bowles. A Verified Algorithm Enumerating Event Structures
    • [M2] Howard Cohl, Moritz Schubotz, Abdou Youssef, André Greiner-Petter, Jürgen Gerhard, Bonita V. Saunders, Marjorie A. McClain, Joon Bang and Kevin Chen. Semantic Preserving Bijective Mappings of Mathematical Formulae between Word Processors and Computer Algebra Systems
    • [M3] Joseph Corneli, Ursula Martin, Dave Murray-Rust and Alison Pease. Towards mathematical AI via a model of the content and process of mathematical question and answer dialogues
    • [M4] William Farmer. Theory Morphisms in Church's Type Theory with Quotation and Evaluation
    • [M5] Ian Ford. Semantic Representation of General Topology in the Wolfram Language
    • [M6] Andreas Holmstrom and Torstein Vik. Zeta types and Tannakian symbols as a method for representing mathematical knowledge
    • [M7] Cezary Kaliszyk and Karol Pąk. Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic
    • [M8] Andrea Kohlhase, Michael Kohlhase and Michael Fürsich. Visual Structure in Math Expressions
    • [M9] Michael Kohlhase, Thomas Koprucki, Dennis Müller and Karsten Tabelow. Mathematical Models as Research Data via Flexiformal Theory Graphs
    • [M10] Zohreh Shams, Mateja Jamink, Gem Stapleton and Yuri Sato. Reasoning with Concept Diagrams about Antipatterns in Ontologies

    Systems & Projects

    • [S1] Nathan Carter and Kenneth Monks. A Web-Based Toolkit for Mathematical Word Processing Applications with Semantics
    • [S2] Jan Jakubuv and Josef Urban. ENIGMA: Efficient Learning-based Inference Guiding Machine
    • [S3] Ekaterina Komendantskaya and Jónathan Heras. Proof mining with dependent types
    • [S4] Adnan Rashid and Osman Hasan. Formalization of Transform Methods using HOL Light
    • [S5] Usman Sanwal and Umair Siddique. Combining Refinement and Signal-Temporal Logic for Biological Systems
    • [S6] Moritz Schubotz, Norman Meuschke, Thomas Hepp, Howard Cohl and Bela Gipp. VMEXT: A Visualization Tool for Mathematical Expression Trees
    • [S7] Abdou Youssef. Part-of-Math Tagging and Applications

    Work in progress

    • [W1] Catherine Dubois, Thérèse Hardin, François Pesseaux and Renaud Rioboo. Proving mathematical libraries: FoCaLiZe polynomials
    • [W2] Carlos E. Freites. Mathdialog: a contextual ZFC syntactical game
    • [W3] Alexander Maletzky. A New Reasoning Framework for Theorema 2.0
    • [W4] Adam Naumowicz. Towards Standardized Mizar Environments
    • [W5] Patrick Ion and Eric Weisstein. The Special Function Concordance

    Business Meetings

    • [B1] Business Meeting
Privacy policy and legal information
Last modified: July 17 2018 16:12:14 CEST