DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2026.7

Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations

Authors: Ricardo Almeida, Blair Archibald, Basile Pesin, and Michele Sevegnani

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract

Commutative regular expressions describe sets of unordered words, and are used, for example, when building type systems for process calculi. In these applications, an important operation is finding the intersection of two expressions, but no algorithm currently exists. We remedy this by proposing an algorithm for computing intersections of commutative regular expressions, which we implement and prove correct in the Rocq prover. The algorithm encodes the intersection of two expressions as systems of linear Diophantine equations, and extracts from their solution an intersection expression. To solve these systems we implement and verify the algorithm proposed by Contejean and Devie. We detail the implementation of the intersection algorithm, highlight essential aspects of the proofs (including the complex proof of termination of the equation system solver), and evaluate the OCaml-extracted solver on random and real-world commutative regular expressions.

Cite as

Ricardo Almeida, Blair Archibald, Basile Pesin, and Michele Sevegnani. Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{almeida_et_al:LIPIcs.ITP.2026.7,
  author =	{Almeida, Ricardo and Archibald, Blair and Pesin, Basile and Sevegnani, Michele},
  title =	{{Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{7:1--7:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.7},
  URN =		{urn:nbn:de:0030-drops-269813},
  doi =		{10.4230/LIPIcs.ITP.2026.7},
  annote =	{Keywords: commutative regular expressions, linear Diophantine equations, interactive theorem provers, Rocq}
}

Search Results

Documents authored by Pesin, Basile

Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations

Abstract

Cite as

Thanks for your feedback!

Could not send message