You must enable JavaScript to use this site
  • FMM 2018 - Third workshop on Formal Mathematics for Mathematicians

    August 13, 2018

    The FMM workshop series allows mathematicians interested in computer assistance and researchers in formal and computer-understandable mathematics to meet and exchange ideas. The meeting provides a platform for discussion of suitable forms of computer assistance between the formal community and interested mathematicians and other researchers.

    The main points of interest include:

    • interactive and automated theorem proving,
    • design of proof languages and techniques,
    • repositories of formalized mathematics,
    • formalization of challenging mathematical problems,
    • development of proof assistants,
    • semantic representation of mathematical knowledge,
    • formal tools in program verification,
    • foundations and philosophy of mathematics,
    • proof assistants in education.

    Invited speaker(s)

    Angeliki Koutsoukou-Argyraki Title: ALEXANDRIA - Large Scale Formal Proof for the Working Mathematician

    ALEXANDRIA is a new ERC project at the University of Cambridge led by Lawrence Paulson aiming at the creation of a proof development environment for working mathematicians through a collaboration of mathematicians and computer scientists. This will be achieved by formalizing mathematical proofs with the proof assistant Isabelle. The focus of the project is the management and use of large-scale mathematical knowledge, both as theorems and as algorithms. In this talk we will briefly discuss some of our objectives and methods. See: Alexandia


    09:00–10:00Angeliki Koutsoukou-Argyraki: Alexandria - Large Scale Formal Proof for the Working Mathematician
    Coffee break
    10:30–11:00Steffen Frerix and Peter Koepke: Automatic Proof-Checking of Ordinary Mathematical Texts
    11:00–11:30Michael Junk, Sebastian Sahli and Stefan Hölle: A Meta Language for Mathematical Reasoning
    11:30–12:00Karol Pąk: Progress in the Formalization of Matiyasevich's theorem in the Mizar system
    12:00–12:30Burak Ekici: Towards Mac Lane's Comparison Theorem for the (co)Kleisli construction in Coq
    Lunch break
    14:00–14:30Slawomir Kolodynski: IsarMathLib - a formalized mathematics library for Isabelle/ZF


    We welcome submission of extended abstracts and demonstration proposals presenting work related to the workshop's points of interest. Electronic submission is done through EasyChair. Extended abstracts and demonstration proposals should be no more than 4 pages formatted in LaTeX using the style onecolceurws (the corresponding style files can be downloaded from here).

    Deadline for submissions: June 10, 2018June 17, 2018
    Notification of acceptance: June 30, 2018

    At least one author of each accepted extended abstract/demonstration proposal is expected to attend FMM and presents his/her extended abstract/demonstration. The extended abstracts will be made available online.

    Programme Committee

    • Yves Bertot, Inria
    • Marco Caminati, University of St Andrews
    • Cezary Kaliszyk, University of Innsbruck (co-chair)
    • Michael Kohlhase, FAU Erlangen-Nürnberg
    • Adam Naumowicz, University of Białystok (co-chair)
    • Aleksy Schubert, University of Warsaw
    • Josef Urban, Czech Technical University in Prague
  • 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: July 17 2018 16:11:50 CEST