The Coq mailing list

[Dennis Müller <dennis.mueller AT fau.de>]

NATURAL FORMAL MATHEMATICS - NatFoM (Call for extended abstracts)

A workshop held between July 26 - 31, 2021 as part of the

14th Conference on Intelligent Computer Mathematics (CICM 2021)

(WILL BE HELD ONLINE OR HYBRID; details to be announced on the CICM website 
https://cicm-conference.org/2021/cicm.php)

In mathematics there has always existed a strong informal sense of 
"naturality". 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 user experience have to become more natural. This workshop, following a 
first edition in 2020, 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 speaker: Jeremy Avigad

Submissions

We call for submissions of extended abstracts (1 page) and demonstration 
proposals presenting work related to the workshop's topics of interest. 
Accepted abstracts can optionally be expanded to full papers (4 to 15 pages) 
to be published in proceedings on ceur-ws.org. To promote Natural Formal 
Mathematics, unfinished or exploratory work will also be welcome.

Electronic submission is done through EasyChair at 
https://easychair.org/conferences/?conf=cicm2021 (select the author role, 
select the "new submission" tab, and choose "NatFom"). Extended abstracts and 
papers should be formatted in LaTeX using the style onecolceurws.

- Submission is continuous (early submit -> early notify).
- July 1. 2021: Final revised papers due
- July 26 - 31. 2021: Workshop (half day; date to be announced)

Accepted abstracts and demonstrations should be presented online and live, to 
allow for questions and discussions.

Program Committee

    Peter Koepke, Bonn (co-chair)
    Dennis Müller, Erlangen (co-chair)
    Merlin Carl, Flensburg
    Marcos Cramer, Dresden
    Michael Junk, Konstanz
    Cezary Kaliszyk, Innsbruck
    Andrea Kohlhase, Neu-Ulm
    Aarne Ranta, Gothenburg
    Josef Urban, Prague

--
Dennis M. Müller

"To do mathematics is to be, at once, touched by fire and bound by reason. 
This is no contradiction. Logic forms a narrow channel through which 
intuition flows with vastly augmented force"
 - Jordan Ellenberg (How Not to Be Wrong)