European Research Network on Formal Proofs
COST action CA20111
COST logo
EU flag and COST acknowledgement
COST (European Cooperation in Science and Technology) is a funding agency for research and innovation networks. Our Actions help connect research initiatives across Europe and enable scientists to grow their ideas by sharing them with their peers. This boosts their research, career and innovation.

This conference is part of the EuroProofNet Symposium. See the symposium page to get information on the other co-located events.

Date: 15-18 September 2025

Venue: Institut Pascal, 530 Rue André Rivière, 91400 Orsay [access] [hotels] [food options]

Organizer: Roussanka Loukanova (rloukanova at gmail)

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

Registration/funding requests: fill in this form (registration is free but mandatory)

Important dates:

Invited speakers: To Be Announced

To give a talk / 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

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

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