Abstract We propose a quantum programming paradigm where all data are familiar classical data, and the only non-classical element is a random number generator that can return results with negative probability. Currently, the vast majority of quantum programming languages instead work with quantum data types made up of qubits. The description of their behavior relies on heavy linear algebra and many interdependent concepts and intuitions from quantum physics, which takes dedicated study to understand. We demonstrate that the proposed view of quantum programming explains its central concepts and constraints in more accessible, computationally relevant terms. This is achieved by systematically reducing everything to the existence of that negative-probability random generator, avoiding mention of advanced physics. This makes quantum programming more accessible to programmers without a deep background in physics or linear algebra. The bulk of this paper is written with such an audience in mind. As a working vehicle, we lay out a simple quantum programming language under this paradigm, showing that not only can it express all quantum algorithms, it also naturally captures the semantics of measurement without ever mentioning qubits or collapse.

Individual fairness testing (Ift) is a framework to find discriminatory instances within a given classifier. In this paper, we show our idea of a Ift framework, that integrates the notion of data validity, termed "Individual Fairness Testing with Data Validity (Ift-v)". We develop a solid foundation of Ift-v and demonstrate the feasibility of Ift-v. Our preliminary evaluation with Ift-v reveals the possibility that many of discriminatory instances detected by state-of-the-art Ift algorithms are considered invalid. These findings prompt a re-think of the current Ift framework, suggesting a transition from solely focusing on the discovery of discriminatory instances to the consideration of valid ones.

We present the design and fail-safety analysis of a sparsely synchronized N-modular redundant architecture for fail-safe computing that can be built on unreliable commercial off-the-shelf (COTS) components. Though the main intended audience is railway operators, the architecture is expected to be useful for general fail-safe computations. Traditional bus-synchronized fail-safe processors have had difficulty catching up with the performance and cost improvements of COTS processors because frequent involvement of the voter needed specialized design that slowed down computations. The proposed architecture alleviates this problem by comparing data much less frequently, only when the data leaves the fail-safe processor altogether. This allows the voter to be vastly simplified, becoming easy to harden against errors. We show empirically the use of COTS hardware barely affects the reliability of the overall architecture, making it as reliable as the simple voting circuitry, with acceptable runtime overhead.

This is an experience report on applying program analysis tools and program monitors to a real-world humanoid robot in simulated and real environments. Humanoid robots, and cyber-physical systems in general, present unique challenges to testing and validation: they have realtime constraints, their runs are typically irreproducible, their tasks are high-level and preclude formal specification, and their software tends to be large and complex. In practice, bugs do cause robots to fail, and methods for analyzing such software has been wanting. This paper presents a case study, in which we find that traditional software bugs like memory errors do cause failures of robots in practice. Dynamic error detectors can be successfully employed to identify such errors - to an extent defined by realtime constraints. Static analysis tools, in their current form, are comparatively of limited use.

Staging is a program generation paradigm with a clean, well-investigated semantics which statically ensures that the generated code is always well-typed and well-scoped. Staging is often used for specializing programs to the known properties or parts of data to improve efficiency, but so far it has been limited to generating terms. This short paper describes our ongoing work on extending staging, with its strong safety guarantees, to generation of non-terms, focusing on ML-style modules. The purpose is to map out the promises and challenges, then to pose a question to solicit the community's expertise in evaluating how essential our extensions are for the purpose of applying staging beyond the realm of terms. We demonstrate our extensions' use in specializing functor applications to eliminate its (currently large) overhead in OCaml. We explain the challenges that those extensions bring in and identify a promising line of attack. Unexpectedly, however, it turns out that we can avoid module generation altogether by representing modules, possibly containing abstract types, as polymorphic records. With the help of first-class modules, module specialization reduces to ordinary term specialization, which can be done with conventional staging. The extent to which this hack generalizes is unclear. Thus we have a question to the community: is there a compelling use case for module generation? With these insights and questions, we offer a starting point for a long-term program in the next stage of staging research.

Abstract We settle three basic questions that naturally arise when verifying code generators written in multi-stage functional programming languages. First, does adding staging to a language compromise any equalities that hold in the base language? Unfortunately it does, and more care is needed to reason about terms with free variables. Second, staging annotations, as the name “annotations” suggests, are often thought to be orthogonal to the behavior of a program, but when is this formally guaranteed to be true? We give termination conditions that characterize when this guarantee holds. Finally, do multi-stage languages satisfy useful, standard extensional properties, for example, that functions agreeing on all arguments are equivalent? We provide a sound and complete notion of applicative bisimulation, which establishes such properties or, in principle, any valid program equivalence. These results yield important insights into staging and allow us to prove the correctness of quite complicated multi-stage programs.

Multi-stage programming (MSP) provides a disciplined approach to run-time code generation. In the purely functional setting, it has been shown how MSP can be used to reduce the overhead of abstractions, allowing clean, maintainable code without paying performance penalties. Unfortunately, MSP is difficult to combine with imperative features, which are prevalent in mainstream languages. The central difficulty is scope extrusion, wherein free variables can inadvertently be moved outside the scopes of their binders. This paper proposes a new approach to combining MSP with imperative features that occupies a "sweet spot" in the design space in terms of how well useful MSP applications can be expressed and how easy it is for programmers to understand. The key insight is that escapes (or "anti-quotes") must be weakly separable from the rest of the code, i.e. the computational effects occurring inside an escape that are visible outside the escape are guaranteed to not contain code. To demonstrate the feasibility of this approach, we formalize a type system based on Lightweight Java which we prove sound, and we also provide an implementation, called Mint, to validate both the expressivity of the type system and the effect of staging on the performance of Java programs.