Twist: sound reasoning for purity and entanglement in Quantum programs

Quantum programming languages enable developers to implement algorithms for quantum computers that promise computational breakthroughs in classically intractable tasks. Programming quantum computers requires awareness of entanglement , the phenomenon in which measurement outcomes of qubits are correlated. Entanglement can determine the correctness of algorithms and suitability of programming patterns. In this work, we formalize purity as a central tool for automating reasoning about entanglement in quantum programs. A pure expression is one whose evaluation is unaffected by the measurement outcomes of qubits that it does not own, implying freedom from entanglement with any other expression in the computation. We present Twist, the first language that features a type system for sound reasoning about purity. The type system enables the developer to identify pure expressions using type annotations. Twist also features purity assertion operators that state the absence of entanglement in the output of quantum gates. To soundly check these assertions, Twist uses a combination of static analysis and runtime verification. We evaluate Twist’s type system and analyses on a benchmark suite of quantum programs in simulation, demonstrating that Twist can express quantum algorithms, catch programming errors in them, and support programs that existing languages disallow, while incurring runtime verification overhead of less than 3.5%.

Decidable Subtyping for Path Dependent Types

<p>Path dependent types form a central component of the Scala programming language. Coupled with other expressive type forms, path dependent types provide for a diverse set of concepts and patterns, from nominality to F-bounded polymorphism. Recent years have seen much work aimed at formalising the foundations of path dependent types, most notably a hard won proof of type safety. Unfortunately subtyping remains undecidable, presenting problems for programmers who rely on the results of their tools. One such tool is Dotty, the basis for the upcoming Scala 3. Another is Wyvern, a new programming language that leverages path dependent types to support both first class modules and parametric polymorphism. In this thesis I investigate the issues with deciding subtyping in Wyvern. I define three decidable variants that retain several key instances of expressiveness including the ability to encode nominality and parametric polymorphism. Wyvfix fixes types to the contexts they are defined in, thereby eliminating expansive environments. Wyvnon-μ removes recursive subtyping, thus removing the key source of expansive environments during subtyping. Wyvμ places a syntactic restriction on the usage of recursive types. I discuss the formal properties of these variants, and the implications each has for expressing the common programming patterns of path dependent types. I have also mechanized the proofs of decidability for both Wyvfix and Wyvμ in Coq.</p>

Decidable Subtyping for Path Dependent Types

<p>Path dependent types form a central component of the Scala programming language. Coupled with other expressive type forms, path dependent types provide for a diverse set of concepts and patterns, from nominality to F-bounded polymorphism. Recent years have seen much work aimed at formalising the foundations of path dependent types, most notably a hard won proof of type safety. Unfortunately subtyping remains undecidable, presenting problems for programmers who rely on the results of their tools. One such tool is Dotty, the basis for the upcoming Scala 3. Another is Wyvern, a new programming language that leverages path dependent types to support both first class modules and parametric polymorphism. In this thesis I investigate the issues with deciding subtyping in Wyvern. I define three decidable variants that retain several key instances of expressiveness including the ability to encode nominality and parametric polymorphism. Wyvfix fixes types to the contexts they are defined in, thereby eliminating expansive environments. Wyvnon-μ removes recursive subtyping, thus removing the key source of expansive environments during subtyping. Wyvμ places a syntactic restriction on the usage of recursive types. I discuss the formal properties of these variants, and the implications each has for expressing the common programming patterns of path dependent types. I have also mechanized the proofs of decidability for both Wyvfix and Wyvμ in Coq.</p>

Reachability types: tracking aliasing and separation in higher-order functional programs

Ownership type systems, based on the idea of enforcing unique access paths, have been primarily focused on objects and top-level classes. However, existing models do not as readily reflect the finer aspects of nested lexical scopes, capturing, or escaping closures in higher-order functional programming patterns, which are increasingly adopted even in mainstream object-oriented languages. We present a new type system, λ * , which enables expressive ownership-style reasoning across higher-order functions. It tracks sharing and separation through reachability sets, and layers additional mechanisms for selectively enforcing uniqueness on top of it. Based on reachability sets, we extend the type system with an expressive flow-sensitive effect system, which enables flavors of move semantics and ownership transfer. In addition, we present several case studies and extensions, including applications to capabilities for algebraic effects, one-shot continuations, and safe parallelization.

Relational nullable types with Boolean unification

We present a simple, practical, and expressive relational nullable type system. A relational nullable type system captures whether an expression may evaluate to null based on its type, but also based on the type of other related expressions. The type system extends the Hindley-Milner type system with Boolean constraints, supports parametric polymorphism, and preserves principal types modulo Boolean equivalence. We show how to support full Hindley-Milner style type inference with an extension of Algorithm W. We conduct a preliminary study of open source projects showing that there is a need for relational nullable type systems across a wide range of programming languages. The most important findings from the study are: (i) programmers use programming patterns where the nullability of one expression depends on the nullability of other related expressions, (ii) such invariants are commonly enforced with run-time exceptions, and (iii) reasoning about these programming patterns requires not only knowledge of when an expression may evaluate to null, but also when it may evaluate to a non-null value. We incorporate these observations in the design of the proposed relational nullable type system.

Transitioning from structural to nominal code with efficient gradual typing

Gradual typing is a principled means for mixing typed and untyped code. But typed and untyped code often exhibit different programming patterns. There is already substantial research investigating gradually giving types to code exhibiting typical untyped patterns, and some research investigating gradually removing types from code exhibiting typical typed patterns. This paper investigates how to extend these established gradual-typing concepts to give formal guarantees not only about how to change types as code evolves but also about how to change such programming patterns as well. In particular, we explore mixing untyped "structural" code with typed "nominal" code in an object-oriented language. But whereas previous work only allowed "nominal" objects to be treated as "structural" objects, we also allow "structural" objects to dynamically acquire certain nominal types, namely interfaces. We present a calculus that supports such "cross-paradigm" code migration and interoperation in a manner satisfying both the static and dynamic gradual guarantees, and demonstrate that the calculus can be implemented efficiently.

High-Level Parallel Ant Colony Optimization with Algorithmic Skeletons

Parallel implementations of swarm intelligence algorithms such as the ant colony optimization (ACO) have been widely used to shorten the execution time when solving complex optimization problems. When aiming for a GPU environment, developing efficient parallel versions of such algorithms using CUDA can be a difficult and error-prone task even for experienced programmers. To overcome this issue, the parallel programming model of Algorithmic Skeletons simplifies parallel programs by abstracting from low-level features. This is realized by defining common programming patterns (e.g. map, fold and zip) that later on will be converted to efficient parallel code. In this paper, we show how algorithmic skeletons formulated in the domain specific language Musket can cope with the development of a parallel implementation of ACO and how that compares to a low-level implementation. Our experimental results show that Musket suits the development of ACO. Besides making it easier for the programmer to deal with the parallelization aspects, Musket generates high performance code with similar execution times when compared to low-level implementations.