[HPSG-L] CfP: MathCompLing for Proofs (MCLP) 2025, Institut Pascal - Call for Participation, Talks, Demos

[Roussanka Loukanova]

Call for Participation, Talks, Demos

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://europroofnet.github.io/MCLP/

Organizer: Roussanka Loukanova

Contact: Roussanka Loukanova <rloukanova at gmail.com>

MCLP is part of the EuroProofNet Symposium:
https://europroofnet.github.io/Symposium/
Date: 8-19 September 2025
https://www.institut-pascal.universite-paris-saclay.fr/en

* 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.

You are welcome to apply for membership in the COST EuroProofNet, if
you work, or want to learn about the areas of any of the topics of
COST EuroProofNet, by joining at least one of its Work Groups (WGs):

https://www.cost.eu/actions/CA20111/
====

Registration for MCLP is free and required for participation and, in
addition, for funding requests.

You are very wellcome to register and participate in MCLP, by funding
from your side.

Applications for reimbursement of travel costs through EuroProofNet is
part of the registration form.

Registration and possible funding requests is by filling in this form:
https://forms.gle/QLFzh3Ugv5WgkhZr7

https://europroofnet.github.io/eligibility/

Important dates:

- May 25 CEST: deadline for registration of participation and possible
funding requests
https://forms.gle/QLFzh3Ugv5WgkhZr7
- June 1 CEST: notification

Invited speakers: To Be Announced

To give a talk or demo, the submission Web page for proposed titles
and abstracts is EasyChair of MCLP 2025:

Submission:
https://easychair.org/conferences?conf=mclp2025

Deadline: May 25 CEST

Please use LaTeX with Springer LNCS package or Microsoft Proceedings
Word Templates:

https://www.springer.com/gp/computer-science/lncs

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.

I 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

====