5 Search Results for "Eades, Peter"

Document

DOI: 10.4230/LIPIcs.FSCD.2024.15

Adjoint Natural Deduction

Authors: Junyoung Jang, Sophia Roshal, Frank Pfenning, and Brigitte Pientka

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

Abstract

Adjoint logic is a general approach to combining multiple logics with different structural properties, including linear, affine, strict, and (ordinary) intuitionistic logics, where each proposition has an intrinsic mode of truth. It has been defined in the form of a sequent calculus because the central concept of independence is most clearly understood in this form, and because it permits a proof of cut elimination following standard techniques. In this paper we present a natural deduction formulation of adjoint logic and show how it is related to the sequent calculus. As a consequence, every provable proposition has a verification (sometimes called a long normal form). We also give a computational interpretation of adjoint logic in the form of a functional language and prove properties of computations that derive from the structure of modes, including freedom from garbage (for modes without weakening and contraction), strictness (for modes disallowing weakening), and erasure (based on a preorder between modes). Finally, we present a surprisingly subtle algorithm for type checking.

Cite as

Junyoung Jang, Sophia Roshal, Frank Pfenning, and Brigitte Pientka. Adjoint Natural Deduction. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 15:1-15:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{jang_et_al:LIPIcs.FSCD.2024.15,
  author =	{Jang, Junyoung and Roshal, Sophia and Pfenning, Frank and Pientka, Brigitte},
  title =	{{Adjoint Natural Deduction}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{15:1--15: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.15},
  URN =		{urn:nbn:de:0030-drops-203441},
  doi =		{10.4230/LIPIcs.FSCD.2024.15},
  annote =	{Keywords: Substructural Logic, Type Systems, Functional Programming}
}

Document

Track A: Algorithms, Complexity and Games

DOI: 10.4230/LIPIcs.ICALP.2024.11

Approximate Counting for Spin Systems in Sub-Quadratic Time

Authors: Konrad Anand, Weiming Feng, Graham Freifeld, Heng Guo, and Jiaheng Wang

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract

We present two randomised approximate counting algorithms with Õ(n^{2-c}/ε²) running time for some constant c > 0 and accuracy ε: 1) for the hard-core model with fugacity λ on graphs with maximum degree Δ when λ = O(Δ^{-1.5-c₁}) where c₁ = c/(2-2c); 2) for spin systems with strong spatial mixing (SSM) on planar graphs with quadratic growth, such as ℤ². For the hard-core model, Weitz’s algorithm (STOC, 2006) achieves sub-quadratic running time when correlation decays faster than the neighbourhood growth, namely when λ = o(Δ^{-2}). Our first algorithm does not require this property and extends the range where sub-quadratic algorithms exist. Our second algorithm appears to be the first to achieve sub-quadratic running time up to the SSM threshold, albeit on a restricted family of graphs. It also extends to (not necessarily planar) graphs with polynomial growth, such as ℤ^d, but with a running time of the form Õ(n²ε^{-2}/2^{c(log n)^{1/d}}) where d is the exponent of the polynomial growth and c > 0 is some constant.

Cite as

Konrad Anand, Weiming Feng, Graham Freifeld, Heng Guo, and Jiaheng Wang. Approximate Counting for Spin Systems in Sub-Quadratic Time. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{anand_et_al:LIPIcs.ICALP.2024.11,
  author =	{Anand, Konrad and Feng, Weiming and Freifeld, Graham and Guo, Heng and Wang, Jiaheng},
  title =	{{Approximate Counting for Spin Systems in Sub-Quadratic Time}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{11:1--11:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.11},
  URN =		{urn:nbn:de:0030-drops-201543},
  doi =		{10.4230/LIPIcs.ICALP.2024.11},
  annote =	{Keywords: Randomised algorithm, Approximate counting, Spin system, Sub-quadratic algorithm}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.ISAAC.2023.2

Faithful Graph Drawing (Invited Talk)

Authors: Seok-Hee Hong

Published in: LIPIcs, Volume 283, 34th International Symposium on Algorithms and Computation (ISAAC 2023)

Abstract

Graph drawing aims to compute good geometric representations of graphs in two or three dimensions. It has wide applications in network visualisation, such as social networks and biological networks, arising from many other disciplines. This talk will review fundamental theoretical results as well as recent advances in graph drawing, including symmetric graph drawing, generalisation of the Tutte’s barycenter theorem, Steinitz’s theorem, and Fáry’s theorem, and the so-called beyond planar graphs such as k-planar graphs. I will conclude my talk with recent progress in visualization of big complex graphs, including sublinear-time graph drawing algorithms and faithful graph drawing.

Cite as

Seok-Hee Hong. Faithful Graph Drawing (Invited Talk). In 34th International Symposium on Algorithms and Computation (ISAAC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 283, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{hong:LIPIcs.ISAAC.2023.2,
  author =	{Hong, Seok-Hee},
  title =	{{Faithful Graph Drawing}},
  booktitle =	{34th International Symposium on Algorithms and Computation (ISAAC 2023)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-289-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{283},
  editor =	{Iwata, Satoru and Kakimura, Naonori},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2023.2},
  URN =		{urn:nbn:de:0030-drops-193044},
  doi =		{10.4230/LIPIcs.ISAAC.2023.2},
  annote =	{Keywords: Graph drawing, Planar graphs, Beyond planar graphs, Tutte’s barycenter theorem, Steinitz’s theorem, F\'{a}ry’s theorem, Sublinear-time graph drawing algorithm, Faithful graph drawing, Symmetric graph drawing}
}

Document

DOI: 10.4230/LIPIcs.ISAAC.2018.39

Polyline Drawings with Topological Constraints

Authors: Emilio Di Giacomo, Peter Eades, Giuseppe Liotta, Henk Meijer, and Fabrizio Montecchiani

Published in: LIPIcs, Volume 123, 29th International Symposium on Algorithms and Computation (ISAAC 2018)

Abstract

Let G be a simple topological graph and let Gamma be a polyline drawing of G. We say that Gamma partially preserves the topology of G if it has the same external boundary, the same rotation system, and the same set of crossings as G. Drawing Gamma fully preserves the topology of G if the planarization of G and the planarization of Gamma have the same planar embedding. We show that if the set of crossing-free edges of G forms a connected spanning subgraph, then G admits a polyline drawing that partially preserves its topology and that has curve complexity at most three (i.e., at most three bends per edge). If, however, the set of crossing-free edges of G is not a connected spanning subgraph, the curve complexity may be Omega(sqrt{n}). Concerning drawings that fully preserve the topology, we show that if G has skewness k, it admits one such drawing with curve complexity at most 2k; for skewness-1 graphs, the curve complexity can be reduced to one, which is a tight bound. We also consider optimal 2-plane graphs and discuss trade-offs between curve complexity and crossing angle resolution of drawings that fully preserve the topology.

Cite as

Emilio Di Giacomo, Peter Eades, Giuseppe Liotta, Henk Meijer, and Fabrizio Montecchiani. Polyline Drawings with Topological Constraints. In 29th International Symposium on Algorithms and Computation (ISAAC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 123, pp. 39:1-39:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{digiacomo_et_al:LIPIcs.ISAAC.2018.39,
  author =	{Di Giacomo, Emilio and Eades, Peter and Liotta, Giuseppe and Meijer, Henk and Montecchiani, Fabrizio},
  title =	{{Polyline Drawings with Topological Constraints}},
  booktitle =	{29th International Symposium on Algorithms and Computation (ISAAC 2018)},
  pages =	{39:1--39:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-094-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{123},
  editor =	{Hsu, Wen-Lian and Lee, Der-Tsai and Liao, Chung-Shou},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2018.39},
  URN =		{urn:nbn:de:0030-drops-99871},
  doi =		{10.4230/LIPIcs.ISAAC.2018.39},
  annote =	{Keywords: Topological graphs, graph drawing, curve complexity, skewness-k graphs, k-planar graphs}
}

Document

DOI: 10.4230/DagSemRep.307

Software Visualization (Dagstuhl Seminar 01211)

Authors: Stephan Diehl, Peter Eades, and John Stasko

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract

Cite as

Stephan Diehl, Peter Eades, and John Stasko. Software Visualization (Dagstuhl Seminar 01211). Dagstuhl Seminar Report 307, pp. 1-35, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2002)

Copy BibTex To Clipboard

@TechReport{diehl_et_al:DagSemRep.307,
  author =	{Diehl, Stephan and Eades, Peter and Stasko, John},
  title =	{{Software Visualization (Dagstuhl Seminar 01211)}},
  pages =	{1--35},
  ISSN =	{1619-0203},
  year =	{2002},
  type = 	{Dagstuhl Seminar Report},
  number =	{307},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.307},
  URN =		{urn:nbn:de:0030-drops-151915},
  doi =		{10.4230/DagSemRep.307},
}

Refine by Author
2 Eades, Peter
1 Anand, Konrad
1 Di Giacomo, Emilio
1 Diehl, Stephan
1 Feng, Weiming
Show More...

Refine by Classification
1 Mathematics of computing → Combinatorics
1 Mathematics of computing → Graph theory
1 Theory of computation → Design and analysis of algorithms
1 Theory of computation → Graph algorithms analysis
1 Theory of computation → Linear logic
Show More...

Refine by Keyword
1 Approximate counting
1 Beyond planar graphs
1 Faithful graph drawing
1 Functional Programming
1 Fáry’s theorem
Show More...

Refine by Type
5 document

Refine by Publication Year
2 2024
1 2002
1 2018
1 2023