9 Search Results for "Pit-Claudel, Clément"

Document
DOI: 10.4230/LIPIcs.CP.2026.24
Formally Verified Certification of Constraint Programming Proofs

Authors: Maarten Flippo, Konstantin Sidorov, Tip ten Brink, Clément Pit-Claudel, and Emir Demirović

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

Abstract
As constraint programming (CP) solvers are increasingly used in critical applications, there is a growing need for certification of solver claims of infeasibility and optimality. Recent work has demonstrated that certification is feasible for CP solvers using a multi-stage proof-generation framework; however, the underlying proof system was informal, and verification relied on translation into an external proof format, impacting the trustworthiness. We address these issues by formalising a rigorous, solver-agnostic framework for certifying CP solver claims. We present a formal definition of DRCP, a proof system for CP over integer domains that captures core solver operations, including conflict analysis and heterogeneous propagation, by modular inference rules with precise semantics. We also develop FznDrcpCheck, a formally verified proof checker in Rocq that validates DRCP proofs directly against FlatZinc models. Our evaluation shows that our framework enables practical certification across various benchmarks with negligible overhead during solving and modest proof-checking costs.
Cite as

Maarten Flippo, Konstantin Sidorov, Tip ten Brink, Clément Pit-Claudel, and Emir Demirović. Formally Verified Certification of Constraint Programming Proofs. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 24:1-24:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{flippo_et_al:LIPIcs.CP.2026.24,
  author =	{Flippo, Maarten and Sidorov, Konstantin and ten Brink, Tip and Pit-Claudel, Cl\'{e}ment and Demirovi\'{c}, Emir},
  title =	{{Formally Verified Certification of Constraint Programming Proofs}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{24:1--24:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.24},
  URN =		{urn:nbn:de:0030-drops-266560},
  doi =		{10.4230/LIPIcs.CP.2026.24},
  annote =	{Keywords: Constraint programming, Proof systems, Certified checking}
}
Document
Artifact
DOI: 10.4230/DARTS.12.1.13
Automatic Layout of Railroad Diagrams (Artifact)

Authors: Shardul Chiplunkar and Clément Pit-Claudel

Published in: DARTS, Volume 12, Issue 1, Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
This artifact contains a Scala implementation of the algorithm described in the accompanying paper, and all resources and instructions necessary to verify the experimental claims made in the paper. The artifact is provided as a Docker image for reproducability. Separately, the latest state of development, which may have diverged from the claims supported by the artifact, can be found at https://github.com/epfl-systemf/librrd.
Cite as

Shardul Chiplunkar and Clément Pit-Claudel. Automatic Layout of Railroad Diagrams (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 13:1-13:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{chiplunkar_et_al:DARTS.12.1.13,
  author =	{Chiplunkar, Shardul and Pit-Claudel, Cl\'{e}ment},
  title =	{{Automatic Layout of Railroad Diagrams (Artifact)}},
  pages =	{13:1--13:8},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2026},
  volume =	{12},
  number =	{1},
  editor =	{Chiplunkar, Shardul and Pit-Claudel, Cl\'{e}ment},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.13},
  URN =		{urn:nbn:de:0030-drops-261509},
  doi =		{10.4230/DARTS.12.1.13},
  annote =	{Keywords: syntax diagram, graph layout, line wrapping, pretty-printing}
}
Artifact
Software
DOI: 10.4230/artifacts.25789
LibRRD

Authors: Shardul Chiplunkar and Clément Pit-Claudel

Abstract
Cite as

Shardul Chiplunkar, Clément Pit-Claudel. LibRRD (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-25789,
   title = {{LibRRD}}, 
   author = {Chiplunkar, Shardul and Pit-Claudel, Cl\'{e}ment},
   note = {Software, version ecoop2026-artifact. (visited on 2026-06-25)},
   url = {https://github.com/epfl-systemf/librrd/releases/tag/ecoop2026-artifact},
   doi = {10.4230/artifacts.25789},
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2026.2
Automatic Layout of Railroad Diagrams

Authors: Shardul Chiplunkar and Clément Pit-Claudel

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
Railroad diagrams (also called "syntax diagrams") are a common, intuitive visualization of grammars, but limited tooling and a lack of formal attention to their layout mostly confines them to hand-drawn documentation. We present the first formal treatment of railroad diagram layout along with a principled, practical implementation. We characterize the problem as compiling a diagram language (specifying conceptual components and how they connect and compose) to a layout language (specifying basic graphical shapes and their sizes and positions). We then implement a compiler that performs line wrapping to meet a target width, as well as vertical alignment and horizontal justification per user-specified policies. We frame line wrapping as optimization, where we describe principled dimensions of optimality and implement corresponding heuristics. For front-end evaluation, we show that our diagram language is well-suited for common applications by describing how regular expressions and Backus-Naur form can be compiled to it. For back-end evaluation, we argue that our compiler is practical by comparing its output to diagrams laid out by hand and by other tools.
Cite as

Shardul Chiplunkar and Clément Pit-Claudel. Automatic Layout of Railroad Diagrams. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 2:1-2:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{chiplunkar_et_al:LIPIcs.ECOOP.2026.2,
  author =	{Chiplunkar, Shardul and Pit-Claudel, Cl\'{e}ment},
  title =	{{Automatic Layout of Railroad Diagrams}},
  booktitle =	{40th European Conference on Object-Oriented Programming (ECOOP 2026)},
  pages =	{2:1--2:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-423-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{372},
  editor =	{Krebbers, Robbert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.2},
  URN =		{urn:nbn:de:0030-drops-260982},
  doi =		{10.4230/LIPIcs.ECOOP.2026.2},
  annote =	{Keywords: syntax diagram, graph layout, line wrapping, pretty-printing}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.5
A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching

Authors: Joshua M. Cohen

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Algebraic data types (ADTs) and pattern matching are widely used to write elegant functional programs and to specify program behavior. These constructs are critical to most general-purpose interactive theorem provers (e.g. Lean, Rocq/Coq), first-order SMT-based deductive verifiers (e.g. Dafny, VeriFast), and intermediate verification languages (e.g. Why3). Such features require layers of compilation - in Rocq, pattern matches are compiled to remove nesting, while SMT-based tools further axiomatize ADTs with a first-order specification. However, these critical steps have been omitted from prior formalizations of such toolchains (e.g. MetaRocq). We give the first proved-sound sophisticated pattern matching compiler (based on Maranget’s compilation to decision trees) and first-order axiomatization of ADTs, both based on Why3 implementations. We prove the soundness of exhaustiveness checking, extending pen-and-paper proofs from the literature, and formulate a robustness property with which we find an exhaustiveness-related bug in Why3. We show that many of our proofs could be useful for reasoning about any first-order program verifier supporting ADTs.
Cite as

Joshua M. Cohen. A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cohen:LIPIcs.ITP.2025.5,
  author =	{Cohen, Joshua M.},
  title =	{{A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{5:1--5:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.5},
  URN =		{urn:nbn:de:0030-drops-246046},
  doi =		{10.4230/LIPIcs.ITP.2025.5},
  annote =	{Keywords: Pattern Matching Compilation, Algebraic Data Types, First-Order Logic}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.16
Finiteness of Symbolic Derivatives in Lean

Authors: Ekaterina Zhuchko, Hendrik Maarand, Margus Veanes, and Gabriel Ebner

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Brzozowski proved that the set of derivatives of any regular expression is finite modulo associativity, idempotence and, notably, commutativity of the union operator. We extend this result to the case of symbolic location based derivatives, for which we prove finiteness of the state space by quotienting only by associativity, deduplication and idempotence (ADI); the fact that we don't use commutativity allows for this result to carry over to the derivative based backtracking (PCRE) match semantics, where the union operator is noncommutative. Furthermore, we consider regular expressions extended with lookarounds, intersection, and negation. We also show that our method for proving finiteness allows us to include certain simplification rules in the derivative operation while preserving finiteness. The finiteness proof is constructive: given an expression R, we construct a finite set that is an overapproximation (modulo ADI) of the set of derivatives of R. We reuse some of the infrastructure provided in previous formalization efforts for regular expressions in Lean 4, showing the flexibility and reusability of the framework.
Cite as

Ekaterina Zhuchko, Hendrik Maarand, Margus Veanes, and Gabriel Ebner. Finiteness of Symbolic Derivatives in Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 16:1-16:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{zhuchko_et_al:LIPIcs.ITP.2025.16,
  author =	{Zhuchko, Ekaterina and Maarand, Hendrik and Veanes, Margus and Ebner, Gabriel},
  title =	{{Finiteness of Symbolic Derivatives in Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{16:1--16:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.16},
  URN =		{urn:nbn:de:0030-drops-246144},
  doi =		{10.4230/LIPIcs.ITP.2025.16},
  annote =	{Keywords: Lean, regular languages, lookarounds, derivatives, finiteness}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.81
Efficient Matching of Some Fundamental Regular Expressions with Backreferences

Authors: Taisei Nogami and Tachio Terauchi

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
Regular expression matching is of practical importance due to its widespread use in real-world applications. In practical use, regular expressions are often used with real-world extensions. Accordingly, the matching problem of regular expressions with real-world extensions has been actively studied in recent years, yielding steady progress. However, backreference, a popular extension supported by most modern programming languages such as Java, Python, JavaScript and others in their standard libraries for string processing, is an exception to this positive trend. In fact, it is known that the matching problem of regular expressions with backreferences (rewbs) is theoretically hard and the existence of an asymptotically fast matching algorithm for arbitrary rewbs seems unlikely. Even among currently known partial solutions, the balance between efficiency and generality remains unsatisfactory. To bridge this gap, we present an efficient matching algorithm for rewbs of the form e_0 (e)_1 e_1 \1 e_2 where e_0, e, e_1, e_2 are pure regular expressions, which are fundamental and frequently used in practical applications. It runs in quadratic time with respect to the input string length, substantially improving the best-known cubic time complexity for these rewbs. Our algorithm combines ideas from both stringology and automata theory in a novel way. We leverage two techniques from automata theory, injection and summarization, to simultaneously examine matches whose backreferenced substrings are either a fixed right-maximal repeat or its extendable prefixes, which are concepts from stringology. By further utilizing a subtle property of extendable prefixes, our algorithm correctly decides the matching problem while achieving the quadratic-time complexity.
Cite as

Taisei Nogami and Tachio Terauchi. Efficient Matching of Some Fundamental Regular Expressions with Backreferences. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 81:1-81:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{nogami_et_al:LIPIcs.MFCS.2025.81,
  author =	{Nogami, Taisei and Terauchi, Tachio},
  title =	{{Efficient Matching of Some Fundamental Regular Expressions with Backreferences}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{81:1--81:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.81},
  URN =		{urn:nbn:de:0030-drops-241886},
  doi =		{10.4230/LIPIcs.MFCS.2025.81},
  annote =	{Keywords: Regular expressions, Backreferences, Regex matching, NFA simulation, Suffix arrays, Right-maximal repeats}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.12
Automatic Goal Clone Detection in Rocq

Authors: Ali Ghanbari

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Proof engineering in Rocq is a labor-intensive process, and as proof developments grow in size, redundancy and maintainability become challenges. One such redundancy is goal cloning, i.e., proving α-equivalent goals multiple times, leading to wasted effort and bloated proof scripts. In this paper, we introduce clone-finder, a novel technique for detecting goal clones in Rocq proofs. By leveraging the formal notion of α-equivalence for Gallina terms, clone-finder systematically identifies duplicated proof goals across large Rocq codebases. We evaluate clone-finder on 40 real-world Rocq projects from the CoqGym dataset. Our results reveal that each project contains an average of 27.73 instances of goal clone. We observed that the clones can be categorized as either exact goal duplication, generalization, or α-equivalent goals with different proofs, each signifying varying levels duplicate effort. Our findings highlight significant untapped potential for proof reuse in Rocq-based formal verification projects, paving the way for future improvements in automated proof engineering.
Cite as

Ali Ghanbari. Automatic Goal Clone Detection in Rocq. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ghanbari:LIPIcs.ECOOP.2025.12,
  author =	{Ghanbari, Ali},
  title =	{{Automatic Goal Clone Detection in Rocq}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{12:1--12:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.12},
  URN =		{urn:nbn:de:0030-drops-233055},
  doi =		{10.4230/LIPIcs.ECOOP.2025.12},
  annote =	{Keywords: Clone Detection, Goal, Proof, Rocq, Gallina}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2017.3
The End of History? Using a Proof Assistant to Replace Language Design with Library Design

Authors: Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, and Katherine Ye

Published in: LIPIcs, Volume 71, 2nd Summit on Advances in Programming Languages (SNAPL 2017)

Abstract
Functionality of software systems has exploded in part because of advances in programming-language support for packaging reusable functionality as libraries. Developers benefit from the uniformity that comes of exposing many interfaces in the same language, as opposed to stringing together hodgepodges of command-line tools. Domain-specific languages may be viewed as an evolution of the power of reusable interfaces, when those interfaces become so flexible as to deserve to be called programming languages. However, common approaches to domain-specific languages give up many of the hard-won advantages of library-building in a rich common language, and even the traditional approach poses significant challenges in learning new APIs. We suggest that instead of continuing to develop new domain-specific languages, our community should embrace library-based ecosystems within very expressive languages that mix programming and theorem proving. Our prototype framework Fiat, a library for the Coq proof assistant, turns languages into easily comprehensible libraries via the key idea of modularizing functionality and performance away from each other, the former via macros that desugar into higher-order logic and the latter via optimization scripts that derive efficient code from logical programs.
Cite as

Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, and Katherine Ye. The End of History? Using a Proof Assistant to Replace Language Design with Library Design. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 3:1-3:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{chlipala_et_al:LIPIcs.SNAPL.2017.3,
  author =	{Chlipala, Adam and Delaware, Benjamin and Duchovni, Samuel and Gross, Jason and Pit-Claudel, Cl\'{e}ment and Suriyakarn, Sorawit and Wang, Peng and Ye, Katherine},
  title =	{{The End of History? Using a Proof Assistant to Replace Language Design with Library Design}},
  booktitle =	{2nd Summit on Advances in Programming Languages (SNAPL 2017)},
  pages =	{3:1--3:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-032-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{71},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2017.3},
  URN =		{urn:nbn:de:0030-drops-71233},
  doi =		{10.4230/LIPIcs.SNAPL.2017.3},
  annote =	{Keywords: Domain-specific languages, synthesis, verification, proof assistants, software development}
}
  • Refine by Type
  • 8 Document/PDF
  • 4 Document/HTML
  • 1 Artifact

  • Refine by Publication Year
  • 4 2026
  • 4 2025
  • 1 2017

  • Refine by Author
  • 5 Pit-Claudel, Clément
  • 3 Chiplunkar, Shardul
  • 1 Chlipala, Adam
  • 1 Cohen, Joshua M.
  • 1 Delaware, Benjamin
  • Show More...

  • Refine by Series/Journal
  • 7 LIPIcs
  • 1 DARTS

  • Refine by Classification
  • 2 Human-centered computing → Visualization
  • 2 Software and its engineering → Software notations and tools
  • 1 Software and its engineering → Formal software verification
  • 1 Software and its engineering → Semantics
  • 1 Software and its engineering → Software maintenance tools
  • Show More...

  • Refine by Keyword
  • 2 graph layout
  • 2 line wrapping
  • 2 pretty-printing
  • 2 syntax diagram
  • 1 Algebraic Data Types
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact