3 Search Results for "Denis, Gaspard"

Document
DOI: 10.4230/LIPIcs.FSCD.2024.21
Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti

Authors: Thiago Felicissimo and Théo Winterhalter

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Proof assistants such as Coq implement a type theory featuring three important features: impredicativity, cumulativity and product covariance. This combination has proven difficult to be expressed in the logical framework Dedukti, and previous attempts have failed in providing an encoding that is proven confluent, sound and conservative. In this work we solve this longstanding open problem by providing an encoding of these three features that we prove to be confluent, sound and to satisfy a restricted (but, we argue, strong enough) form of conservativity. Our proof of confluence is a contribution by itself, and combines various criteria and proof techniques from rewriting theory. Our proof of soundness also contributes a new strategy in which the result is shown in terms of an inverse translation function, fixing a common flaw made in some previous encoding attempts.
Cite as

Thiago Felicissimo and Théo Winterhalter. Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{felicissimo_et_al:LIPIcs.FSCD.2024.21,
  author =	{Felicissimo, Thiago and Winterhalter, Th\'{e}o},
  title =	{{Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{21:1--21:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.21},
  URN =		{urn:nbn:de:0030-drops-203503},
  doi =		{10.4230/LIPIcs.FSCD.2024.21},
  annote =	{Keywords: Dedukti, Rewriting, Confluence, Dependent types, Cumulativity, Universes}
}
Document
DOI: 10.4230/LIPIcs.AofA.2020.11
Asymptotics of Minimal Deterministic Finite Automata Recognizing a Finite Binary Language

Authors: Andrew Elvey Price, Wenjie Fang, and Michael Wallner

Published in: LIPIcs, Volume 159, 31st International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms (AofA 2020)

Abstract
We show that the number of minimal deterministic finite automata with n+1 states recognizing a finite binary language grows asymptotically for n → ∞ like Θ(n! 8ⁿ e^{3 a₁ n^{1/3}} n^{7/8}), where a₁ ≈ -2.338 is the largest root of the Airy function. For this purpose, we use a new asymptotic enumeration method proposed by the same authors in a recent preprint (2019). We first derive a new two-parameter recurrence relation for the number of such automata up to a given size. Using this result, we prove by induction tight bounds that are sufficiently accurate for large n to determine the asymptotic form using adapted Netwon polygons.
Cite as

Andrew Elvey Price, Wenjie Fang, and Michael Wallner. Asymptotics of Minimal Deterministic Finite Automata Recognizing a Finite Binary Language. In 31st International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms (AofA 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 159, pp. 11:1-11:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{elveyprice_et_al:LIPIcs.AofA.2020.11,
  author =	{Elvey Price, Andrew and Fang, Wenjie and Wallner, Michael},
  title =	{{Asymptotics of Minimal Deterministic Finite Automata Recognizing a Finite Binary Language}},
  booktitle =	{31st International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms (AofA 2020)},
  pages =	{11:1--11:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-147-4},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{159},
  editor =	{Drmota, Michael and Heuberger, Clemens},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AofA.2020.11},
  URN =		{urn:nbn:de:0030-drops-120419},
  doi =		{10.4230/LIPIcs.AofA.2020.11},
  annote =	{Keywords: Airy function, asymptotics, directed acyclic graphs, Dyck paths, bijection, stretched exponential, compacted trees, minimal automata, finite languages}
}
Document
DOI: 10.4230/LIPIcs.SEA.2018.24
Fast Spherical Drawing of Triangulations: An Experimental Study of Graph Drawing Tools

Authors: Luca Castelli Aleardi, Gaspard Denis, and Éric Fusy

Published in: LIPIcs, Volume 103, 17th International Symposium on Experimental Algorithms (SEA 2018)

Abstract
We consider the problem of computing a spherical crossing-free geodesic drawing of a planar graph: this problem, as well as the closely related spherical parameterization problem, has attracted a lot of attention in the last two decades both in theory and in practice, motivated by a number of applications ranging from texture mapping to mesh remeshing and morphing. Our main concern is to design and implement a linear time algorithm for the computation of spherical drawings provided with theoretical guarantees. While not being aesthetically pleasing, our method is extremely fast and can be used as initial placer for spherical iterative methods and spring embedders. We provide experimental comparison with initial placers based on planar Tutte parameterization. Finally we explore the use of spherical drawings as initial layouts for (Euclidean) spring embedders: experimental evidence shows that this greatly helps to untangle the layout and to reach better local minima.
Cite as

Luca Castelli Aleardi, Gaspard Denis, and Éric Fusy. Fast Spherical Drawing of Triangulations: An Experimental Study of Graph Drawing Tools. In 17th International Symposium on Experimental Algorithms (SEA 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 103, pp. 24:1-24:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{aleardi_et_al:LIPIcs.SEA.2018.24,
  author =	{Aleardi, Luca Castelli and Denis, Gaspard and Fusy, \'{E}ric},
  title =	{{Fast Spherical Drawing of Triangulations: An Experimental Study of Graph Drawing Tools}},
  booktitle =	{17th International Symposium on Experimental Algorithms (SEA 2018)},
  pages =	{24:1--24:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-070-5},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{103},
  editor =	{D'Angelo, Gianlorenzo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2018.24},
  URN =		{urn:nbn:de:0030-drops-89597},
  doi =		{10.4230/LIPIcs.SEA.2018.24},
  annote =	{Keywords: Graph drawing, planar triangulations, spherical parameterizations}
}
  • Refine by Author
  • 1 Aleardi, Luca Castelli
  • 1 Denis, Gaspard
  • 1 Elvey Price, Andrew
  • 1 Fang, Wenjie
  • 1 Felicissimo, Thiago
  • Show More...

  • Refine by Classification
  • 1 Mathematics of computing → Enumeration
  • 1 Mathematics of computing → Generating functions
  • 1 Mathematics of computing → Graph theory
  • 1 Theory of computation → Equational logic and rewriting
  • 1 Theory of computation → Regular languages
  • Show More...

  • Refine by Keyword
  • 1 Airy function
  • 1 Confluence
  • 1 Cumulativity
  • 1 Dedukti
  • 1 Dependent types
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2018
  • 1 2020
  • 1 2024

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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