8 Search Results for "W�chner, Patrick"

Document
DOI: 10.4230/LIPIcs.ITP.2023.24
An Extensible User Interface for Lean 4

Authors: Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
Contemporary proof assistants rely on complex automation and process libraries with millions of lines of code. At these scales, understanding the emergent interactions between components can be a serious challenge. One way of managing complexity, long established in informal practice, is through varying external representations. For instance, algebraic notation facilitates term-based reasoning whereas geometric diagrams invoke spatial intuition. Objects viewed one way become much simpler than when viewed differently. In contrast, modern general-purpose ITP systems usually only support limited, textual representations. Treating this as a problem of human-computer interaction, we aim to demonstrate that presentations - UI elements that store references to the objects they are displaying - are a fruitful way of thinking about ITP interface design. They allow us to make headway on two fronts - introspection of prover internals and support for diagrammatic reasoning. To this end we have built an extensible user interface for the Lean 4 prover with an associated ProofWidgets 4 library of presentation-based UI components. We demonstrate the system with several examples including type information popups, structured traces, contextual suggestions, a display for algebraic reasoning, and visualizations of red-black trees. Our interface is already part of the core Lean distribution.
Cite as

Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner. An Extensible User Interface for Lean 4. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 24:1-24:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{nawrocki_et_al:LIPIcs.ITP.2023.24,
  author =	{Nawrocki, Wojciech and Ayers, Edward W. and Ebner, Gabriel},
  title =	{{An Extensible User Interface for Lean 4}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{24:1--24:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.24},
  URN =		{urn:nbn:de:0030-drops-183991},
  doi =		{10.4230/LIPIcs.ITP.2023.24},
  annote =	{Keywords: user interfaces, human-computer interaction, Lean}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2023.55
Combinatorial Depth Measures for Hyperplane Arrangements

Authors: Patrick Schnider and Pablo Soberón

Published in: LIPIcs, Volume 258, 39th International Symposium on Computational Geometry (SoCG 2023)

Abstract
Regression depth, introduced by Rousseeuw and Hubert in 1999, is a notion that measures how good of a regression hyperplane a given query hyperplane is with respect to a set of data points. Under projective duality, this can be interpreted as a depth measure for query points with respect to an arrangement of data hyperplanes. The study of depth measures for query points with respect to a set of data points has a long history, and many such depth measures have natural counterparts in the setting of hyperplane arrangements. For example, regression depth is the counterpart of Tukey depth. Motivated by this, we study general families of depth measures for hyperplane arrangements and show that all of them must have a deep point. Along the way we prove a Tverberg-type theorem for hyperplane arrangements, giving a positive answer to a conjecture by Rousseeuw and Hubert from 1999. We also get three new proofs of the centerpoint theorem for regression depth, all of which are either stronger or more general than the original proof by Amenta, Bern, Eppstein, and Teng. Finally, we prove a version of the center transversal theorem for regression depth.
Cite as

Patrick Schnider and Pablo Soberón. Combinatorial Depth Measures for Hyperplane Arrangements. In 39th International Symposium on Computational Geometry (SoCG 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 258, pp. 55:1-55:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{schnider_et_al:LIPIcs.SoCG.2023.55,
  author =	{Schnider, Patrick and Sober\'{o}n, Pablo},
  title =	{{Combinatorial Depth Measures for Hyperplane Arrangements}},
  booktitle =	{39th International Symposium on Computational Geometry (SoCG 2023)},
  pages =	{55:1--55:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-273-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{258},
  editor =	{Chambers, Erin W. and Gudmundsson, Joachim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2023.55},
  URN =		{urn:nbn:de:0030-drops-179055},
  doi =		{10.4230/LIPIcs.SoCG.2023.55},
  annote =	{Keywords: Depth measures, Hyperplane arrangements, Regression depth, Tverberg theorem}
}
Document
DOI: 10.4230/LIPIcs.SWAT.2022.16
Well-Separation and Hyperplane Transversals in High Dimensions

Authors: Helena Bergold, Daniel Bertschinger, Nicolas Grelier, Wolfgang Mulzer, and Patrick Schnider

Published in: LIPIcs, Volume 227, 18th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2022)

Abstract
A family of k point sets in d dimensions is well-separated if the convex hulls of any two disjoint subfamilies can be separated by a hyperplane. Well-separation is a strong assumption that allows us to conclude that certain kinds of generalized ham-sandwich cuts for the point sets exist. But how hard is it to check if a given family of high-dimensional point sets has this property? Starting from this question, we study several algorithmic aspects of the existence of transversals and separations in high-dimensions. First, we give an explicit proof that k point sets are well-separated if and only if their convex hulls admit no (k - 2)-transversal, i.e., if there exists no (k - 2)-dimensional flat that intersects the convex hulls of all k sets. It follows that the task of checking well-separation lies in the complexity class coNP. Next, we show that it is NP-hard to decide whether there is a hyperplane-transversal (that is, a (d - 1)-transversal) of a family of d + 1 line segments in ℝ^d, where d is part of the input. As a consequence, it follows that the general problem of testing well-separation is coNP-complete. Furthermore, we show that finding a hyperplane that maximizes the number of intersected sets is NP-hard, but allows for an Ω((log k)/(k log log k))-approximation algorithm that is polynomial in d and k, when each set consists of a single point. When all point sets are finite, we show that checking whether there exists a (k - 2)-transversal is in fact strongly NP-complete. Finally, we take the viewpoint of parametrized complexity, using the dimension d as a parameter: given k convex sets in ℝ^d, checking whether there is a (k-2)-transversal is FPT with respect to d. On the other hand, for k ≥ d+1 finite point sets in ℝ^d, it turns out that checking whether there is a (d-1)-transversal is W[1]-hard with respect to d.
Cite as

Helena Bergold, Daniel Bertschinger, Nicolas Grelier, Wolfgang Mulzer, and Patrick Schnider. Well-Separation and Hyperplane Transversals in High Dimensions. In 18th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 227, pp. 16:1-16:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bergold_et_al:LIPIcs.SWAT.2022.16,
  author =	{Bergold, Helena and Bertschinger, Daniel and Grelier, Nicolas and Mulzer, Wolfgang and Schnider, Patrick},
  title =	{{Well-Separation and Hyperplane Transversals in High Dimensions}},
  booktitle =	{18th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2022)},
  pages =	{16:1--16:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-236-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{227},
  editor =	{Czumaj, Artur and Xin, Qin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SWAT.2022.16},
  URN =		{urn:nbn:de:0030-drops-161766},
  doi =		{10.4230/LIPIcs.SWAT.2022.16},
  annote =	{Keywords: hyperplane transversal, high-dimension, hardness}
}
Document
DOI: 10.4230/LIPIcs.ITP.2021.4
A Graphical User Interface Framework for Formal Verification

Authors: Edward W. Ayers, Mateja Jamnik, and W. T. Gowers

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract
We present the "ProofWidgets" framework for implementing general user interfaces (UIs) within an interactive theorem prover. The framework uses web technology and functional reactive programming, as well as metaprogramming features of advanced interactive theorem proving (ITP) systems to allow users to create arbitrary interactive UIs for representing the goal state. Users of the framework can create GUIs declaratively within the ITP’s metaprogramming language, without having to develop in multiple languages and without coordinated changes across multiple projects, which improves development time for new designs of UI. The ProofWidgets framework also allows UIs to make use of the full context of the theorem prover and the specialised libraries that ITPs offer, such as methods for dealing with expressions and tactics. The framework includes an extensible structured pretty-printing engine that enables advanced interaction with expressions such as interactive term rewriting. We exemplify the framework with an implementation for the https://leanprover-community.github.io. The framework is already in use by hundreds of contributors to the Lean mathematical library.
Cite as

Edward W. Ayers, Mateja Jamnik, and W. T. Gowers. A Graphical User Interface Framework for Formal Verification. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 4:1-4:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{ayers_et_al:LIPIcs.ITP.2021.4,
  author =	{Ayers, Edward W. and Jamnik, Mateja and Gowers, W. T.},
  title =	{{A Graphical User Interface Framework for Formal Verification}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{4:1--4:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.4},
  URN =		{urn:nbn:de:0030-drops-138996},
  doi =		{10.4230/LIPIcs.ITP.2021.4},
  annote =	{Keywords: User Interfaces, ITP}
}
Document
DOI: 10.4230/LIPIcs.SEA.2021.7
Engineering Predecessor Data Structures for Dynamic Integer Sets

Authors: Patrick Dinklage, Johannes Fischer, and Alexander Herlez

Published in: LIPIcs, Volume 190, 19th International Symposium on Experimental Algorithms (SEA 2021)

Abstract
We present highly optimized data structures for the dynamic predecessor problem, where the task is to maintain a set S of w-bit numbers under insertions, deletions, and predecessor queries (return the largest element in S no larger than a given key). The problem of finding predecessors can be viewed as a generalized form of the membership problem, or as a simple version of the nearest neighbour problem. It lies at the core of various real-world problems such as internet routing. In this work, we engineer (1) a simple implementation of the idea of universe reduction, similar to van-Emde-Boas trees (2) variants of y-fast tries [Willard, IPL'83], and (3) B-trees with different strategies for organizing the keys contained in the nodes, including an implementation of dynamic fusion nodes [Pǎtraşcu and Thorup, FOCS'14]. We implement our data structures for w = 32,40,64, which covers most typical scenarios. Our data structures finish workloads faster than previous approaches while being significantly more space-efficient, e.g., they clearly outperform standard implementations of the STL by finishing up to four times as fast using less than a third of the memory. Our tests also provide more general insights on data structure design, such as how small sets should be stored and handled and if and when new CPU instructions such as advanced vector extensions pay off.
Cite as

Patrick Dinklage, Johannes Fischer, and Alexander Herlez. Engineering Predecessor Data Structures for Dynamic Integer Sets. In 19th International Symposium on Experimental Algorithms (SEA 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 190, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{dinklage_et_al:LIPIcs.SEA.2021.7,
  author =	{Dinklage, Patrick and Fischer, Johannes and Herlez, Alexander},
  title =	{{Engineering Predecessor Data Structures for Dynamic Integer Sets}},
  booktitle =	{19th International Symposium on Experimental Algorithms (SEA 2021)},
  pages =	{7:1--7:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-185-6},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{190},
  editor =	{Coudert, David and Natale, Emanuele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2021.7},
  URN =		{urn:nbn:de:0030-drops-137799},
  doi =		{10.4230/LIPIcs.SEA.2021.7},
  annote =	{Keywords: integer data structures, dynamic data structures, predecessor, universe reduction, y-fast trie, fusion tree, B-tree}
}
Document
DOI: 10.4230/LIPIcs.CPM.2017.15
Lempel-Ziv Compression in a Sliding Window

Authors: Philip Bille, Patrick Hagge Cording, Johannes Fischer, and Inge Li Gørtz

Published in: LIPIcs, Volume 78, 28th Annual Symposium on Combinatorial Pattern Matching (CPM 2017)

Abstract
We present new algorithms for the sliding window Lempel-Ziv (LZ77) problem and the approximate rightmost LZ77 parsing problem. Our main result is a new and surprisingly simple algorithm that computes the sliding window LZ77 parse in O(w) space and either O(n) expected time or O(n log log w+z log log s) deterministic time. Here, w is the window size, n is the size of the input string, z is the number of phrases in the parse, and s is the size of the alphabet. This matches the space and time bounds of previous results while removing constant size restrictions on the alphabet size. To achieve our result, we combine a simple modification and augmentation of the suffix tree with periodicity properties of sliding windows. We also apply this new technique to obtain an algorithm for the approximate rightmost LZ77 problem that uses O(n(log z + log log n)) time and O(n) space and produces a (1+e)-approximation of the rightmost parsing (any constant e>0). While this does not improve the best known time-space trade-offs for exact rightmost parsing, our algorithm is significantly simpler and exposes a direct connection between sliding window parsing and the approximate rightmost matching problem.
Cite as

Philip Bille, Patrick Hagge Cording, Johannes Fischer, and Inge Li Gørtz. Lempel-Ziv Compression in a Sliding Window. In 28th Annual Symposium on Combinatorial Pattern Matching (CPM 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 78, pp. 15:1-15:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bille_et_al:LIPIcs.CPM.2017.15,
  author =	{Bille, Philip and Cording, Patrick Hagge and Fischer, Johannes and G{\o}rtz, Inge Li},
  title =	{{Lempel-Ziv Compression in a Sliding Window}},
  booktitle =	{28th Annual Symposium on Combinatorial Pattern Matching (CPM 2017)},
  pages =	{15:1--15:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-039-2},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{78},
  editor =	{K\"{a}rkk\"{a}inen, Juha and Radoszewski, Jakub and Rytter, Wojciech},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CPM.2017.15},
  URN =		{urn:nbn:de:0030-drops-73316},
  doi =		{10.4230/LIPIcs.CPM.2017.15},
  annote =	{Keywords: Lempel-Ziv parsing, sliding window, rightmost matching}
}
Document
DOI: 10.4230/LIPIcs.TQC.2013.157
Towards Efficient Decoding of Classical-Quantum Polar Codes

Authors: Mark M. Wilde, Olivier Landon-Cardinal, and Patrick Hayden

Published in: LIPIcs, Volume 22, 8th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2013)

Abstract
Known strategies for sending bits at the capacity rate over a general channel with classical input and quantum output (a cq channel) require the decoder to implement impractically complicated collective measurements. Here, we show that a fully collective strategy is not necessary in order to recover all of the information bits. In fact, when coding for a large number N uses of a cq channel W, N*I(W_{acc}) of the bits can be recovered by a non-collective strategy which amounts to coherent quantum processing of the results of product measurements, where I(W_{acc}) is the accessible information of the channel W. In order to decode the other N(I(W)-I(W_{acc})) bits, where I(W) is the Holevo rate, our conclusion is that the receiver should employ collective measurements. We also present two other results: 1) collective Fuchs-Caves measurements (quantum likelihood ratio measurements) can be used at the receiver to achieve the Holevo rate and 2) we give an explicit form of the Helstrom measurements used in small-size polar codes. The main approach used to demonstrate these results is a quantum extension of Arikan's polar codes.
Cite as

Mark M. Wilde, Olivier Landon-Cardinal, and Patrick Hayden. Towards Efficient Decoding of Classical-Quantum Polar Codes. In 8th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 22, pp. 157-177, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{wilde_et_al:LIPIcs.TQC.2013.157,
  author =	{Wilde, Mark M. and Landon-Cardinal, Olivier and Hayden, Patrick},
  title =	{{Towards Efficient Decoding of Classical-Quantum Polar Codes}},
  booktitle =	{8th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2013)},
  pages =	{157--177},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-55-2},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{22},
  editor =	{Severini, Simone and Brandao, Fernando},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TQC.2013.157},
  URN =		{urn:nbn:de:0030-drops-43141},
  doi =		{10.4230/LIPIcs.TQC.2013.157},
  annote =	{Keywords: classical-quantum channel, classical-quantum polar codes, quantum likelihood ratio, quantum successive cancellation decoder}
}
Document
DOI: 10.4230/DagSemProc.07461.15
Structured Markov Chains Arising from Finite-Source Retrial Queues with Orital Search

Authors: Patrick Wüchner, János Sztrik, and Hermann de Meer

Published in: Dagstuhl Seminar Proceedings, Volume 7461, Numerical Methods for Structured Markov Chains (2008)

Abstract
We consider retrial queueing systems with a finite number of homogeneous sources of calls, a single reliable server, and the search for orbiting customers by the server after job completion. During this investigation, the infinitesimal generator of the underlying (finite) continuous-time Markov chain takes a (level-dependent) QBD-like form. After solving for the steady state probabilities using the MOSEL-2 tool, the results show a surprising maximum of the mean response time. This maximum was already discovered by other researchers dealing with finite-source retrial queues. However, to our best knowledge, no thorough investigation was done yet why this maximum exists and in which way it depends on the system parameters. In the talk, after introducing the backgrounds of finite-source retrial queues with orbital search, a generalized stochastic Petri net is used to derive the underlying continuous-time Markov chain and its generator. Finally, using the seminar, we can hopefully bring forward discussions how to make more general statements on the parameter-dependent behavior of the response time’s maximum.
Cite as

Patrick Wüchner, János Sztrik, and Hermann de Meer. Structured Markov Chains Arising from Finite-Source Retrial Queues with Orital Search. In Numerical Methods for Structured Markov Chains. Dagstuhl Seminar Proceedings, Volume 7461, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{wuchner_et_al:DagSemProc.07461.15,
  author =	{W\"{u}chner, Patrick and Sztrik, J\'{a}nos and de Meer, Hermann},
  title =	{{Structured Markov Chains Arising from Finite-Source Retrial Queues with Orital Search}},
  booktitle =	{Numerical Methods for Structured Markov Chains},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7461},
  editor =	{Dario Bini and Beatrice Meini and Vaidyanathan Ramaswami and Marie-Ange Remiche and Peter Taylor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07461.15},
  URN =		{urn:nbn:de:0030-drops-13895},
  doi =		{10.4230/DagSemProc.07461.15},
  annote =	{Keywords: Structured Markov chain, finite source, retrial queues, orbital search, performance measures, performance tool}
}
  • Refine by Author
  • 2 Ayers, Edward W.
  • 2 Fischer, Johannes
  • 2 Schnider, Patrick
  • 1 Bergold, Helena
  • 1 Bertschinger, Daniel
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Computational geometry
  • 1 Human-centered computing → Visualization systems and tools
  • 1 Mathematics of computing → Combinatorics
  • 1 Software and its engineering → Functional languages
  • 1 Software and its engineering → Software usability
  • Show More...

  • Refine by Keyword
  • 1 B-tree
  • 1 Depth measures
  • 1 Hyperplane arrangements
  • 1 ITP
  • 1 Lean
  • Show More...

  • Refine by Type
  • 8 document

  • Refine by Publication Year
  • 2 2021
  • 2 2023
  • 1 2008
  • 1 2013
  • 1 2017
  • Show More...

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