[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
====
CfP: MathCompLing for Proofs (MCLP) 2025, Institut Pascal - Call for Talks,
Demos, Participation
====
Call for Talks, Demos, Participation
International Conference on
Mathematical and Computational Linguistics for Proofs, MCLP
Date: 15-18 September 2025
Venue: Institut Pascal, 530 Rue André Rivière, 91400 Orsay
https://urldefense.com/v3/__https://europroofnet.github.io/MCLP/__;!!IBzWLUs!USx6v0yAYYVVPl6F5Z9UeNsAYjPTZQ8kHMFBgQr-zYPHNU3St_Mm5XGj4i_l2vHmDh4Z2XijQkR6cMu11kKRLUzDC8Kr988eMWZt6ElWHRc$
Organisers:
Roussanka Loukanova
and
Axel Ljungström
Contact: Roussanka Loukanova <[email protected]<mailto:[email protected]>>
Axel Ljungström <[email protected]<mailto:[email protected]>>
MCLP is part of the EuroProofNet Symposium:
https://urldefense.com/v3/__https://europroofnet.github.io/Symposium/__;!!IBzWLUs!USx6v0yAYYVVPl6F5Z9UeNsAYjPTZQ8kHMFBgQr-zYPHNU3St_Mm5XGj4i_l2vHmDh4Z2XijQkR6cMu11kKRLUzDC8Kr988eMWZtb06AVak$
Date: 8-19 September 2025
https://urldefense.com/v3/__https://www.institut-pascal.universite-paris-saclay.fr/en__;!!IBzWLUs!USx6v0yAYYVVPl6F5Z9UeNsAYjPTZQ8kHMFBgQr-zYPHNU3St_Mm5XGj4i_l2vHmDh4Z2XijQkR6cMu11kKRLUzDC8Kr988eMWZtpSklla0$
COST Action EuroProofNet
https://urldefense.com/v3/__https://www.cost.eu/actions/CA20111/__;!!IBzWLUs!USx6v0yAYYVVPl6F5Z9UeNsAYjPTZQ8kHMFBgQr-zYPHNU3St_Mm5XGj4i_l2vHmDh4Z2XijQkR6cMu11kKRLUzDC8Kr988eMWZtzU1sH1Y$
* NOTE: To participate in MCLP, including by giving a talk or demo, you do not
need to work currently and directly on proofs and verification. These fields
are in active developments. Your strong interest in contributing to such work
is important.
Registration for MCLP is free and required for participation.
Registration form is accessible on the website of the EuroProofNet Symposium:
https://urldefense.com/v3/__https://forms.gle/QLFzh3Ugv5WgkhZr7__;!!IBzWLUs!USx6v0yAYYVVPl6F5Z9UeNsAYjPTZQ8kHMFBgQr-zYPHNU3St_Mm5XGj4i_l2vHmDh4Z2XijQkR6cMu11kKRLUzDC8Kr988eMWZtU2mZ14c$
https://urldefense.com/v3/__https://europroofnet.github.io/eligibility/__;!!IBzWLUs!USx6v0yAYYVVPl6F5Z9UeNsAYjPTZQ8kHMFBgQr-zYPHNU3St_Mm5XGj4i_l2vHmDh4Z2XijQkR6cMu11kKRLUzDC8Kr988eMWZtrN2_0jk$
You are very welcome to register and participate in MCLP, by funding from your
side. There might be some (small) possibility for funding from COST Action
EuroProofNet.
Applications for reimbursement of travel costs through EuroProofNet is part of
the registration form.
To give a talk or demo, the submission Web page for proposed titles and
abstracts is EasyChair of MCLP 2025:
Submission:
https://urldefense.com/v3/__https://easychair.org/conferences?conf=mclp2025__;!!IBzWLUs!USx6v0yAYYVVPl6F5Z9UeNsAYjPTZQ8kHMFBgQr-zYPHNU3St_Mm5XGj4i_l2vHmDh4Z2XijQkR6cMu11kKRLUzDC8Kr988eMWZt9pe-CRQ$
Deadline: still open for contributed talks, by funding from your side.
Please use LaTeX with Springer LNCS package or Microsoft Proceedings Word
Templates:
https://urldefense.com/v3/__https://www.springer.com/gp/computer-science/lncs__;!!IBzWLUs!USx6v0yAYYVVPl6F5Z9UeNsAYjPTZQ8kHMFBgQr-zYPHNU3St_Mm5XGj4i_l2vHmDh4Z2XijQkR6cMu11kKRLUzDC8Kr988eMWZtoJu_wmM$
The abstract should be short, about 1/2 page, and in addition, as many
references as you reasonably need. You will have the possibility to update it
around the time of the MCLP.
We shall arrange publications in two stages:
(1) by Institut Pascal, proceedings of talks and presentations
(2) post conference special volume of extended papers
====
**DESCRIPTION:**
Mathematical and computational linguistics for proofs. Mathematical linguistics
(MathLing) is an interdisciplinary area providing theoretical foundations of
computer science, as well as syntax and semantics of natural and formal
languages, including for mathematical logic in theorem provers, proof
assistants, model checkers, verification of programs, software and hardware.
Computational linguistics (CompLing) is a subfield of MathLing, which provides
computational processing of formal and natural (human) languages by
computational theories and algorithms for:
- Parsing formal and natural languages in mathematics
- Computational syntax-semantics interfaces
- Computational processing of language, by mathematical logic and other
approaches, e.g., graphical, diagrammatic, numerical, algebraic, statistical,
and other related methods
- New hybrid integrations of approaches of mathematical logic and other methods.
**OBJECTIVES:**
MCLP aims at initiating new directions of research on the use of natural
language in proof assistants, provers, and other related systems.
MCLP covers the following areas of theories and applications, from the
perspectives of current and future use of natural language in proof systems:
- Mathematical theories, with a focus on computational approaches to formal and
natural languages
- Type Theories, including Dependent Type Theories
- Applications in domain specific areas, for using provers, in areas of
mathematics
- Applications to other domain specific areas, e.g., health systems, medical
sciences, forensics, judiciary proceedings, legal laws, transport, etc.
- Specialised formal, specification, and natural languages, e.g., specific
fragments and instances depending on domains of specific areas, or generalized
over groups of domains.
The program of MCLP shall include talks, presentations, and sessions of
discussions.
The focus is on computational approaches to natural language used in
mathematical texts.
**TOPICS:**
We invite contributed talks, in the above areas, relevant to the following
topics, with a focus on formal and natural language in proof and verification
systems, without being limited to them:
- Theories of Computation
- Theories of Information
- Type Theories
- Computational Methods of Inferences in Natural Language
- Computational Theories and Systems of Reasoning in Natural Language
- Transfer of reasoning in natural language to theorem provers, or vice versa
- Transfer of reasoning between natural language, theorem provers, model
checkers, and various computational assistants
- Translations between natural language of mathematics and formal languages of
proof and verification systems
- Computational Grammar, Syntax, Semantics, Syntax-Semantics Interfaces
- Interfaces between morphology, lexicon, syntax, semantics, speech, text,
pragmatics, with a focus on mathematical texts
- Parsing of formal and natural language
- Multilingual Processing
- Large-Scale Grammars of Natural Languages
- Controlled Languages of Mathematics
- Interdisciplinary, Integrated, and Hybrid Methods
====
