6 Search Results for "Bertrand, Clément"

Document
DOI: 10.4230/LIPIcs.SoCG.2026.37
A Free Lunch: Manifolds of Positive Reach Can Be Smoothed Without Decreasing the Reach

Authors: Hana Dal Poz Kouřimská, André Lieutier, and Mathijs Wintraecken

Published in: LIPIcs, Volume 367, 42nd International Symposium on Computational Geometry (SoCG 2026)

Abstract
Assumptions on the reach are crucial for ensuring the correctness of many geometric and topological algorithms, including triangulation, manifold reconstruction and learning, homotopy reconstruction, and methods for estimating curvature or reach. However, these assumptions are often coupled with the requirement that the manifold be smooth, typically at least C². In this paper, we prove that any manifold with positive reach can be approximated arbitrarily well by a C^∞ manifold without significantly reducing the reach. More precisely, given a manifold with reach R, we construct a manifold that is ε-close to it in the C¹ sense (both the manifold and its tangent spaces are close), and has reach at least R-ε. The proof employs techniques from differential topology - partitions of unity and smoothing using convolution kernels. This result implies that nearly all theorems established for C² or manifolds with a certain reach naturally extend to manifolds with the same reach, even if they are not C², for free!
Cite as

Hana Dal Poz Kouřimská, André Lieutier, and Mathijs Wintraecken. A Free Lunch: Manifolds of Positive Reach Can Be Smoothed Without Decreasing the Reach. In 42nd International Symposium on Computational Geometry (SoCG 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 367, pp. 37:1-37:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{dalpozkourimska_et_al:LIPIcs.SoCG.2026.37,
  author =	{Dal Poz Kou\v{r}imsk\'{a}, Hana and Lieutier, Andr\'{e} and Wintraecken, Mathijs},
  title =	{{A Free Lunch: Manifolds of Positive Reach Can Be Smoothed Without Decreasing the Reach}},
  booktitle =	{42nd International Symposium on Computational Geometry (SoCG 2026)},
  pages =	{37:1--37:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-418-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{367},
  editor =	{Ahn, Hee-Kap and Hoffmann, Michael and Nayyeri, Amir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2026.37},
  URN =		{urn:nbn:de:0030-drops-258434},
  doi =		{10.4230/LIPIcs.SoCG.2026.37},
  annote =	{Keywords: Reach, Manifolds, Smoothing, Differentiability, Differential topology}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2026.74
Manifolds of Positive Reach, Differentiability, Tangent Variation, and Attaining the Reach

Authors: André Lieutier and Mathijs Wintraecken

Published in: LIPIcs, Volume 367, 42nd International Symposium on Computational Geometry (SoCG 2026)

Abstract
This paper contains three main results. Firstly, we give an elementary proof of the following statement: Let ℳ be a topological manifold without boundary embedded in R^d. If ℳ has positive reach, then ℳ can locally be written as the graph of a C^{1,1} function from the tangent space to the normal space. Conversely if ℳ can locally be written as the graph of a C^{1,1} function from the tangent space to the normal space, then ℳ has positive reach. The result was hinted at by Federer when he introduced the reach, and proved by Lytchak. Lytchak’s proof relies heavily on CAT(k)-theory. The proof presented here uses only basic results on homology. Secondly, we give optimal Lipschitz-constants for the derivative, in other words we give an optimal bound for the angle between tangent spaces in term of the distance between the points. We stress that Lytchak did not provide any bound, let alone an optimal one, making his proof, although interesting from a mathematical perspective, ineffectual in an algorithmic setting. To provide precise and optimal bounds on the angle between tangent spaces, we formally introduce the local reach for sets of positive reach, based on Aamari et al.’s discussion for C² manifolds. We prove that the local reach of a manifold is completely characterized by the variation of tangent spaces. This improves earlier results, that were either suboptimal or assumed that the manifold was C². Thirdly, we show that the value of the reach is equals minimum of the local reach of the set and a global bottleneck for any set. This generalizes a result by Aamari et al. which explains how the reach is attained for C² manifolds.
Cite as

André Lieutier and Mathijs Wintraecken. Manifolds of Positive Reach, Differentiability, Tangent Variation, and Attaining the Reach. In 42nd International Symposium on Computational Geometry (SoCG 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 367, pp. 74:1-74:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{lieutier_et_al:LIPIcs.SoCG.2026.74,
  author =	{Lieutier, Andr\'{e} and Wintraecken, Mathijs},
  title =	{{Manifolds of Positive Reach, Differentiability, Tangent Variation, and Attaining the Reach}},
  booktitle =	{42nd International Symposium on Computational Geometry (SoCG 2026)},
  pages =	{74:1--74:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-418-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{367},
  editor =	{Ahn, Hee-Kap and Hoffmann, Michael and Nayyeri, Amir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2026.74},
  URN =		{urn:nbn:de:0030-drops-258812},
  doi =		{10.4230/LIPIcs.SoCG.2026.74},
  annote =	{Keywords: Reach, Manifolds, Differentiability class, Lipschitz continuity, Tangent space}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2026.92
Estimation of Conformal Metrics

Authors: Jérôme Taupin

Published in: LIPIcs, Volume 367, 42nd International Symposium on Computational Geometry (SoCG 2026)

Abstract
We study deformations of the geodesic distances on a domain of ℝ^N induced by a function called conformal factor. We show that under a positive reach assumption on the domain (not necessarily a submanifold) and mild assumptions on the conformal factor, geodesics for the conformal metric have good regularity properties in the form of a lower bounded reach. This regularity allows for efficient estimation of the conformal metric from a random point cloud with a relative error proportional to the Hausdorff distance between the point cloud and the original domain. We then establish convergence rates of order n^{-1/d} that are close to sharp when the intrinsic dimension d of the domain is large, for an estimator that can be computed in O(n²) time. Finally, this paper includes a useful equivalence result between ball graphs and nearest-neighbors graphs when assuming Ahlfors regularity of the sampling measure, allowing to transpose results from one setting to another.
Cite as

Jérôme Taupin. Estimation of Conformal Metrics. In 42nd International Symposium on Computational Geometry (SoCG 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 367, pp. 92:1-92:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{taupin:LIPIcs.SoCG.2026.92,
  author =	{Taupin, J\'{e}r\^{o}me},
  title =	{{Estimation of Conformal Metrics}},
  booktitle =	{42nd International Symposium on Computational Geometry (SoCG 2026)},
  pages =	{92:1--92:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-418-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{367},
  editor =	{Ahn, Hee-Kap and Hoffmann, Michael and Nayyeri, Amir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2026.92},
  URN =		{urn:nbn:de:0030-drops-258986},
  doi =		{10.4230/LIPIcs.SoCG.2026.92},
  annote =	{Keywords: Geometric inference, metric estimation, conformal metric, geodesics, sets of positive reach}
}
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.CONCUR.2023.33
Complexity of Membership and Non-Emptiness Problems in Unbounded Memory Automata

Authors: Clément Bertrand, Cinzia Di Giusto, Hanna Klaudel, and Damien Regnault

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
We study the complexity relationship between three models of unbounded memory automata: nu-automata (ν-A), Layered Memory Automata (LaMA)and History-Register Automata (HRA). These are all extensions of finite state automata with unbounded memory over infinite alphabets. We prove that the membership problem is NP-complete for all of them, while they fall into different classes for what concerns non-emptiness. The problem of non-emptiness is known to be Ackermann-complete for HRA, we prove that it is PSPACE-complete for ν-A.
Cite as

Clément Bertrand, Cinzia Di Giusto, Hanna Klaudel, and Damien Regnault. Complexity of Membership and Non-Emptiness Problems in Unbounded Memory Automata. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 33:1-33:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2023.33,
  author =	{Bertrand, Cl\'{e}ment and Di Giusto, Cinzia and Klaudel, Hanna and Regnault, Damien},
  title =	{{Complexity of Membership and Non-Emptiness Problems in Unbounded Memory Automata}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{33:1--33:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.33},
  URN =		{urn:nbn:de:0030-drops-190277},
  doi =		{10.4230/LIPIcs.CONCUR.2023.33},
  annote =	{Keywords: memory automata, \nu-automata, LaMA, HRA, complexity, non-emptiness, membership}
}
Document
DOI: 10.4230/LITES-v006-i001-a002
Improving WCET Evaluation using Linear Relation Analysis

Authors: Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Erwan Jahier, Nicolas Halbwachs, Fabienne Carrier, Mihail Asavoae, and Rémy Boutonnet

Published in: LITES, Volume 6, Issue 1 (2019). Leibniz Transactions on Embedded Systems, Volume 6, Issue 1

Abstract
The precision of a worst case execution time (WCET) evaluation tool on a given program is highly dependent on how the tool is able to detect and discard semantically infeasible executions of the program. In this paper, we propose to use the classical abstract interpretation-based method of linear relation analysis to discover and exploit relations between execution paths. For this purpose, we add auxiliary variables (counters) to the program to trace its execution paths. The results are easily incorporated in the classical workflow of a WCET evaluator, when the evaluator is based on the popular implicit path enumeration technique. We use existing tools - a WCET evaluator and a linear relation analyzer - to build and experiment a prototype implementation of this idea.
Cite as

Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Erwan Jahier, Nicolas Halbwachs, Fabienne Carrier, Mihail Asavoae, and Rémy Boutonnet. Improving WCET Evaluation using Linear Relation Analysis. In LITES, Volume 6, Issue 1 (2019). Leibniz Transactions on Embedded Systems, Volume 6, Issue 1, pp. 02:1-02:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{raymond_et_al:LITES-v006-i001-a002,
  author =	{Raymond, Pascal and Maiza, Claire and Parent-Vigouroux, Catherine and Jahier, Erwan and Halbwachs, Nicolas and Carrier, Fabienne and Asavoae, Mihail and Boutonnet, R\'{e}my},
  title =	{{Improving WCET Evaluation using Linear Relation Analysis}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{02:1--02:28},
  ISSN =	{2199-2002},
  year =	{2019},
  volume =	{6},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v006-i001-a002},
  URN =		{urn:nbn:de:0030-drops-192784},
  doi =		{10.4230/LITES-v006-i001-a002},
  annote =	{Keywords: Worst Case Execution Time estimation, Infeasible Execution Paths, Abstract Interpretation}
}
  • Refine by Type
  • 6 Document/PDF
  • 4 Document/HTML

  • Refine by Publication Year
  • 3 2026
  • 1 2025
  • 1 2023
  • 1 2019

  • Refine by Author
  • 2 Lieutier, André
  • 2 Wintraecken, Mathijs
  • 1 Asavoae, Mihail
  • 1 Bertrand, Clément
  • 1 Boutonnet, Rémy
  • Show More...

  • Refine by Series/Journal
  • 5 LIPIcs
  • 1 LITES

  • Refine by Classification
  • 3 Theory of computation → Computational geometry
  • 1 Software and its engineering → Real-time systems software
  • 1 Software and its engineering → Semantics
  • 1 Theory of computation → Automata over infinite objects
  • 1 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 2 Manifolds
  • 2 Reach
  • 1 Abstract Interpretation
  • 1 Algebraic Data Types
  • 1 Differentiability
  • 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