NFM 2020 - Workshop on Natural Formal Mathematics
July 30, 2020
The workshop will take place virtually using the same login details as the CICM conference.
See here for the program.
In (pure) mathematics there has always existed a strong informal sense
of "naturality" of topics and methods. Generally "natural" theories,
notions, properties, or proofs are prefered over technical, convoluted,
or counterintuitive approaches. If formal mathematics is to become part
of mainstream mathematics, its formalizations and usage apparently have
to become more "natural". Or should mathematicians learn formal
languages like Lean so that they regard them as natural? This workshop
broadly addresses the issue of naturality in formal mathematics.
Topics of interest include (but are not limited to):
- The notion of naturality in mathematics generally
- Natural input and output languages for formal mathematics systems
- Parsing natural mathematical language
- Controlled natural languages (CNL) for mathematics
- Making formal mathematics documents readable
- Naturality of foundational theories (types, sets, HOL, ...)
- Naturality of proof methods
- Natural proof structures and granularities
- Natural structurings of formalized mathematical texts and libraries
- Mathematical type setting (LaTeX) and formal mathematics
- Examples of natural formalizations
Invited Talks
Accepted Papers
- Formalizing Foundational Notions in Naproche-SAD, Peter Koepke, Jan Penquitt, Marcel Schütz, Erik Sturzenhecker
- How Natural is Formal Mathematics?, Michael Junk, Sebastian Sahli
- Integrating Formal Methods into LaTeX Workflows, Dennis Müller, Michael Kohlhase
- Why We Need Structured Proofs in Mathematics, Mauricio Ayala-Rincón, Gabriel Ferreira Silva
Submissions
We welcome submission of extended abstracts and demonstration proposals
presenting work related to the workshop's topics of interest. Electronic
submission is done through EasyChair. Extended abstracts and
demonstration proposals should 1 page formatted in LaTeX using the style
onecolceurws (the corresponding style files can be downloaded from here).
- Submission deadline: June 15 2020 (or later pending further developments of the CICM organization)
- Notification of acceptance: July 01 2020
The submission is via easychair.
At least one author of each accepted extended abstract/demonstration
proposal is expected to attend NFM and presents his/her extended
abstract/demonstration. The extended abstracts will be made available
online.
Program Committee
- Florian Rabe, Erlangen (co-chair)
- Peter Koepke, Bonn (co-chair)
- Marcos Cramer, Dresden
- Michael Junk, Konstanz
- Cezary Kaliszyk, Innsbruck
- Andrea Kohlhase, Neu-Ulm
- Aarne Ranta, Gothenburg
- Josef Urban, Prague
|