In an oblivious signature, a receiver can obtain a signature from the signer for a message in the specified message set. It satisfies unforgeability and blind property similar to blind signature, and in-addition satisfies constrained-message property, i.e. the signer can only obtain valid signatures from the specified message set. Most existing oblivious signature protocols have communication complexity that's linearly proportional to the message set size, which makes the applications less scalable. Another common issue is they usually do not satisfy unlinkable, i.e. the signer cannot map a signature back to a specific run/receiver. In this work, we propose a generic construction of oblivious signature protocol from a set-membership NIZK and a blind signature protocol. Our construction has communication complexity that does not grow linearly with respect to the message set, and preserves unlinkability from the underlying blind signature protocol.

Compact closed categories include objects representing higher-order functions and are well-established as models of linear logic, concurrency, and quantum computing. We show that it is possible to construct such compact closed categories for conventional sum and product types by defining a dual to sum types, a negative type, and a dual to product types, a fractional type. Inspired by the categorical semantics, we define a sound operational semantics for negative and fractional types in which a negative type represents a computational effect that ``reverses execution flow'' and a fractional type represents a computational effect that ``garbage collects'' particular values or throws exceptions. Specifically, we extend a first-order reversible language of type isomorphisms with negative and fractional types, specify an operational semantics for each extension, and prove that each extension forms a compact closed category. We furthermore show that both operational semantics can be merged using the standard combination of backtracking and exceptions resulting in a smooth interoperability of negative and fractional types. We illustrate the expressiveness of this combination by writing a reversible SAT solver that uses backtracking search along freshly allocated and de-allocated locations. The operational semantics, most of its meta-theoretic properties, and all examples are formalized in a supplementary Agda package.

In this paper, genetic algorithms are proposed to shrink counterexamples found by QuickChick, a property-based testing framework for Coq. In order to make the outcome of property-based testing humanly understandable and inspectable, genetic algorithms are brought into the realm of rigorous software development as shrinkers capable of handling a broad range of data structures. In the present study, two showcases, merge sort and insertion of red-black trees, are investigated for illustrative purposes. Due to the lack of relevant results existing in the literature, two baseline methods, random sample and random walk are included in the experiments for comparison with the proposed genetic algorithm. The obtained results indicate that the proposal is effective since the program mistake can be identified with ease by examining the shrunk counterexamples and also that the adopted genetic algorithm statistically significantly outperforms random sample and random walk in both counterexample sizes and running time.

A key part of implementing high-level languages is providing built- in and default data structures. Yet selecting good defaults is hard. A mutable data structure’s workload is not known in advance, and it may shift over its lifetime—e.g., between read-heavy and write- heavy, or from heavy contention by multiple threads to single- threaded or low-frequency use. One idea is to switch implementa- tions adaptively, but it is nontrivial to switch the implementation of a concurrent data structure at runtime. Performing the transition requires a concurrent snapshot of data structure contents, which normally demands special engineering in the data structure’s de- sign. However, in this paper we identify and formalize an relevant property of lock-free algorithms. Namely, lock-freedom is su cient to guarantee that freezing memory locations in an arbitrary order will result in a valid snapshot. Several functional languages have data structures that freeze and thaw, transitioning between mutable and immutable, such as Haskell vectors and Clojure transients, but these enable only single-threaded writers. We generalize this approach to augment an arbitrary lock-free data structure with the ability to gradually freeze and optionally transition to a new representation. This aug- mentation doesn’t require changing the algorithm or code for the data structure, only replacing its datatype for mutable references with a freezable variant. In this paper, we present an algorithm for lifting plain to adaptive data and prove that the resulting hy- brid data structure is itself lock-free, linearizable, and simulates the original. We also perform an empirical case study in the context of heating up and cooling down concurrent maps.

Mathematical theorems are human knowledge able to be accumulated in the form of symbolic representation, and proving theorems has been considered intelligent behavior. Based on the BHK interpretation and the Curry-Howard isomorphism, proof assistants, software capable of interacting with human for constructing formal proofs, have been developed in the past several decades. Since proofs can be considered and expressed as programs, proof assistants simplify and verify a proof by computationally evaluating the program corresponding to the proof. Thanks to the transformation from logic to computation, it is now possible to generate or search for formal proofs directly in the realm of computation. Evolutionary algorithms, known to be flexible and versatile, have been successfully applied to handle a variety of scientific and engineering problems in numerous disciplines for also several decades. Examining the feasibility of establishing the link between evolutionary algorithms, as the program generator, and proof assistants, as the proof verifier, in order to automatically find formal proofs to a given logic sentence is the primary goal of this study. In the article, we describe in detail our first, ad-hoc attempt to fully automatically prove theorems as well as the preliminary results. Ten simple theorems from various branches of mathematics were proven, and most of these theorems cannot be proven by using the tactic auto alone in Coq, the adopted proof assistant. The implication and potential influence of this study are discussed, and the developed source code with the obtained experimental results are released as open source.

An adaptive discretization method, called split-on-demand (SoD), enables estimation of distribution algorithms (EDAs) for discrete variables to solve continuous optimization problems. SoD randomly splits a continuous interval if the number of search points within the interval exceeds a threshold, which is decreased at every iteration. After the split operation, the nonempty intervals are assigned integer codes, and the search points are discretized accordingly. As an example of using SoD with EDAs, the integration of SoD and the extended compact genetic algorithm (ECGA) is presented and numerically examined. In this integration, we adopt a local search mechanism as an optional component of our back end optimization engine. As a result, the proposed framework can be considered as a memetic algorithm, and SoD can potentially be applied to other memetic algorithms. The numerical experiments consist of two parts: (1) a set of benchmark functions on which ECGA with SoD and ECGA with two well-known discretization methods: the fixed-height histogram (FHH) and the fixed-width histogram (FWH) are compared; (2) a real-world application, the economic dispatch problem, on which ECGA with SoD is compared to other methods. The experimental results indicate that SoD is a better discretization method to work with ECGA. Moreover, ECGA with SoD works quite well on the economic dispatch problem and delivers solutions better than the best known results obtained by other methods in existence.

In this paper, we propose a new approach that consists of the extended compact genetic algorithm (ECGA) and split-on-demand (SoD), an adaptive discretization technique, to economic dispatch (ED) problems with nonsmooth cost functions. ECGA is designed for handling problems with decision variables of the discrete type, while the decision variables of ED problems are oftentimes real numbers. Thus, in order to employ ECGA to tackle ED problems, SoD is utilized for discretizing the continuous decision variables and works as the interface between ECGA and the ED problem. Furthermore, ED problems in practice are usually hard for traditional mathematical programming methodologies because of the equality and inequality constraints. Hence, in addition to integrating ECGA and SoD, in this study, we devise a repair operator specifically for making the infeasible solutions to satisfy the equality constraint. To examine the performance and effectiveness, we apply the proposed framework to two different-sized ED problems with nonsmooth cost function considering the valve-point effects. The experimental results are compared to those obtained by various evolutionary algorithms and demonstrate that handling ED problems with the proposed framework is a promising research direction.

This paper proposes an adaptive discretization method, called Split-on-Demand (SoD), to enable the probabilistic model building genetic algorithm (PMBGA) to solve optimization problems in the continuous domain. The procedure, effect, and usage of SoD are described in detail. As an example, the integration of SoD and the extended compact genetic algorithm (ECGA), named real-coded ECGA (rECGA), is presented and numerically examined. The experimental results indicate that rECGA works well and SoD is effective. The behavior of SoD is analyzed and discussed, followed by the potential future work for SoD.