| 1. |
- Abel, Andreas, 1974
(author)
-
On model-theoretic strong normalization for truth-table natural deduction
- 2021
-
In: Leibniz International Proceedings in Informatics, LIPIcs. - Schloss Dagstuhl : Leibniz Zentrum für Informatik. - 1868-8969.
-
Conference paper (peer-reviewed)abstract
- Intuitionistic truth table natural deduction (ITTND) by Geuvers and Hurkens (2017), which is inherently non-confluent, has been shown strongly normalizing (SN) using continuation-passing-style translations to parallel lambda calculus by Geuvers, van der Giessen, and Hurkens (2019). We investigate the applicability of standard model-theoretic proof techniques and show (1) SN of detour reduction (β) using Girard's reducibility candidates, and (2) SN of detour and permutation reduction (βπ) using biorthogonals. In the appendix, we adapt Tait's method of saturated sets to β, clarifying the original proof of 2017, and extend it to βπ.
|
|
| 2. |
- Abrahamsson, Oskar, 1986, et al.
(author)
-
Candle: A Verified Implementation of HOL Light
- 2022
-
In: Leibniz International Proceedings in Informatics, LIPIcs. - 1868-8969. ; 237
-
Conference paper (peer-reviewed)abstract
- This paper presents a fully verified interactive theorem prover for higher-order logic, more specifically: a fully verified clone of HOL Light. Our verification proof of this new system results in an end-to-end correctness theorem that guarantees the soundness of the entire system down to the machine code that executes at runtime. Our theorem states that every exported fact produced by this machine-code program is valid in higher-order logic. Our implementation consists of a read-eval-print loop (REPL) that executes the CakeML compiler internally. Throughout this work, we have strived to make the REPL of the new system provide a user experience as close to HOL Light's as possible. To this end, we have, e.g., made the new system parse the same variant of OCaml syntax as HOL Light. All of the work described in this paper has been carried out in the HOL4 theorem prover.
|
|
| 3. |
- Abrahamsson, Oskar, 1986, et al.
(author)
-
Fast, Verified Computation for Candle
- 2023
-
In: Leibniz International Proceedings in Informatics, LIPIcs. - 1868-8969. ; 268
-
Conference paper (peer-reviewed)abstract
- This paper describes how we have added an efficient function for computation to the kernel of the Candle interactive theorem prover. Candle is a CakeML port of HOL Light which we have, in prior work, proved sound w.r.t. the inference rules of the higher-order logic. This paper extends the original implementation and soundness proof with a new kernel function for fast computation. Experiments show that the new computation function is able to speed up certain evaluation proofs by several orders of magnitude.
|
|
| 4. |
- Adams, Robin, 1978, et al.
(author)
-
A Type Theory for Probabilistic and Bayesian Reasoning
- 2018
-
In: Leibniz International Proceedings in Informatics (LIPIcs). - 1868-8969. - 9783959770309 ; 69, s. 11-134
-
Conference paper (peer-reviewed)abstract
- This paper introduces a novel type theory and logic for probabilistic reasoning. Its logic is quantitative, with fuzzy predicates. It includes normalisation and conditioning of states. This conditioning uses a key aspect that distinguishes our probabilistic type theory from quantum type theory, namely the bijective correspondence between predicates and side-effect free actions (called instrument, or assert, maps). The paper shows how suitable computation rules can be derived from this predicate-action correspondence, and uses these rules for calculating conditional probabilities in two well-known examples of Bayesian reasoning in (graphical) models. Our type theory may thus form the basis for a mechanisation of Bayesian inference.
|
|
| 5. |
- Afshari, Bahareh, 1981, et al.
(author)
-
A Cyclic Proof System for Full Computation Tree Logic
- 2023
-
In: Leibniz International Proceedings in Informatics, LIPIcs Volume 2521, February 2023, EACSL Annual Conference on Computer Science Logic, CSL 2023, Warsaw, 13 February 2023 through 16 February 2023. - Leibniz-Zentrum fur Informatik : Dagstuhl Publishing. - 1868-8969. - 9783959772648
-
Conference paper (peer-reviewed)
|
|
| 6. |
- Ashvinkumar, Vikrant, et al.
(author)
-
Local Routing in Sparse and Lightweight Geometric Graphs
- 2019
-
In: LIPICS. - : Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. ; 149, s. 1-30
-
Conference paper (peer-reviewed)abstract
- Online routing in a planar embedded graph is central to a number of fields and has been studied extensively in the literature. For most planar graphs no O(1)-competitive online routing algorithm exists. A notable exception is the Delaunay triangulation for which Bose and Morin showed that there exists an online routing algorithm that is O(1)-competitive. However, a Delaunay triangulation can have Omega(n) vertex degree and a total weight that is a linear factor greater than the weight of a minimum spanning tree. We show a simple construction, given a set V of n points in the Euclidean plane, of a planar geometric graph on V that has small weight (within a constant factor of the weight of a minimum spanning tree on V), constant degree, and that admits a local routing strategy that is O(1)-competitive. Moreover, the technique used to bound the weight works generally for any planar geometric graph whilst preserving the admission of an O(1)-competitive routing strategy.
|
|
| 7. |
- Atalar, Aras, 1985, et al.
(author)
-
How lock-free data structures perform in dynamic environments: Models and analyses
- 2017
-
In: Leibniz International Proceedings in Informatics, LIPIcs. - 1868-8969. - 9783959770316 ; 70, s. 23.1-23.17
-
Conference paper (peer-reviewed)abstract
- © Aras Atalar, Paul Renaud-Goud, and Philippas Tsigas.In this paper we present two analytical frameworks for calculating the performance of lock-free data structures. Lock-free data structures are based on retry loops and are called by application-specific routines. In contrast to previous work, we consider in this paper lock-free data structures in dynamic environments. The size of each of the retry loops, and the size of the application routines invoked in between, are not constant but may change dynamically. The new frameworks follow two different approaches. The first framework, the simplest one, is based on queuing theory. It introduces an average-based approach that facilitates a more coarse-grained analysis, with the benefit of being ignorant of size distributions. Because of this independence from the distribution nature it covers a set of complicated designs. The second approach, instantiated with an exponential distribution for the size of the application routines, uses Markov chains, and is tighter because it constructs stochastically the execution, step by step. Both frameworks provide a performance estimate which is close to what we observe in practice. We have validated our analysis on (i) several fundamental lock-free data structures such as stacks, queues, deques and counters, some of them employing helping mechanisms, and (ii) synthetic tests covering a wide range of possible lock-free designs. We show the applicability of our results by introducing new back-off mechanisms, tested in application contexts, and by designing an efficient memory management scheme that typical lock-free algorithms can utilize.
|
|
| 8. |
- Atalar, Aras, 1985, et al.
(author)
-
Lock-Free Search Data Structures: Throughput Modeling with Poisson Processes
- 2019
-
In: Leibniz International Proceedings in Informatics, LIPIcs. - 1868-8969. ; 125
-
Conference paper (peer-reviewed)abstract
- This paper considers the modeling and the analysis of the performance of lock-free concurrent search data structures. Our analysis considers such lock-free data structures that are utilized through a sequence of operations which are generated with a memoryless and stationary access pattern. Our main contribution is a new way of analyzing lock-free concurrent search data structures: our execution model matches with the behavior that we observe in practice and achieves good throughput predictions. Search data structures are formed of basic blocks, usually referred to as nodes, which can be accessed by two kinds of events, characterized by their latencies; (i) CAS events originated as a result of modifications of the search data structure (ii) Read events that occur during traversals. An operation triggers a set of events, and the running time of an operation is computed as the sum of the latencies of these events. We identify the factors that impact the latency of such events on a multi-core shared memory system. The main challenge (though not the only one) is that the latency of each event mainly depends on the state of the caches at the time when it is triggered, and the state of caches is changing due to events that are triggered by the operations of any thread in the system. Accordingly, the latency of an event is determined by the ordering of the events on the timeline. Search data structures are usually designed to accommodate a large number of nodes, which makes the occurrence of an event on a given node rare at any given time. In this context, we model the events on each node as Poisson processes from which we can extract the frequency and probabilistic ordering of events that are used to estimate the expected latency of an operation, and in turn the throughput. We have validated our analysis on several fundamental lock-free search data structures such as linked lists, hash tables, skip lists and binary trees.
|
|
| 9. |
- Becker, Heiko, et al.
(author)
-
Verified Compilation and Optimization of Floating-Point Programs in CakeML
- 2022
-
In: Leibniz International Proceedings in Informatics, LIPIcs. - : Schloss Dagstuhl - Leibniz-Zentrum für Informatik. - 1868-8969. ; 222
-
Conference paper (peer-reviewed)abstract
- Verified compilers such as CompCert and CakeML have become increasingly realistic over the last few years, but their support for floating-point arithmetic has thus far been limited. In particular, they lack the “fast-math-style” optimizations that unverified mainstream compilers perform. Supporting such optimizations in the setting of verified compilers is challenging because these optimizations, for the most part, do not preserve the IEEE-754 floating-point semantics. However, IEEE-754 floating-point numbers are finite approximations of the real numbers, and we argue that any compiler correctness result for fast-math optimizations should appeal to a real-valued semantics rather than the rigid IEEE-754 floating-point numbers. This paper presents RealCake, an extension of CakeML that achieves end-to-end correctness results for fast-math-style optimized compilation of floating-point arithmetic. This result is achieved by giving CakeML a flexible floating-point semantics and integrating an external proof-producing accuracy analysis. RealCake's end-to-end theorems relate the I/O behavior of the original source program under real-number semantics to the observable I/O behavior of the compiler generated and fast-math-optimized machine code.
|
|
| 10. |
- Bezem, Marc, et al.
(author)
-
A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic
- 2018
-
In: Leibniz International Proceedings in Informatics, LIPIcs. - 1868-8969. ; 97
-
Conference paper (peer-reviewed)abstract
- The univalence axiom expresses the principle of extensionality for dependent type theory. However, if we simply add the univalence axiom to type theory, then we lose the property of canonicity— that every closed term computes to a canonical form. A computation becomes ‘stuck’ when it reaches the point that it needs to evaluate a proof term that is an application of the univalence axiom. So we wish to find a way to compute with the univalence axiom. While this problem has been solved with the formulation of cubical type theory, where the computations are expressed using a nominal extension of lambda-calculus, it may be interesting to explore alternative solutions, which do not require such an extension.As a first step, we present here a system of propositional higher-order minimal logic (PHOML). There are three kinds of typing judgement in PHOML. There are terms which inhabit types, which are the simple types over Ω. There are proofs which inhabit propositions, which are the terms of type Ω. The canonical propositions are those constructed from ⊥ by implication ⊃. Thirdly, there are paths which inhabit equations M = A N , where M and N are terms of type A. There are two ways to prove an equality: reflexivity, and propositional extensionality — logically equivalent propositions are equal. This system allows for some definitional equalities that are not present in cubical type theory, namely that transport along the trivial path is identity. We present a call-by-name reduction relation for this system, and prove that the system satisfies canonicity: every closed typable term head-reduces to a canonical form. This work has been formalised in Agda.
|
|
