MFPS 2018 Program

Quipper is a functional programming language for quantum computation which has been used to implement various elaborate quantum algorithms. At the moment, Quipper is implemented as an embedded language, whose host language is Haskell. One of the disadvantages to Quipper being an embedded language is that the Haskell type system, while providing many type-safety properties, is not in general strong enough to ensure the full type-safety of quantum programs.

The Proto-Quipper language provides a foundation for the development of a stand-alone (i.e., non-embedded) version of Quipper. Like Quipper, Proto-Quipper acts as a circuit description language and provides the ability to treat circuits as data in order to manipulate them as a whole. However, Proto-Quipper is also designed to “enforce the physics”, in the sense that its type system would detect, at compile-time, programming errors that could lead to ill-formed or undefined circuits.

I will start my talk with a brief introduction to quantum computing and a discussion of the design principles behind Quipper. I will then present Proto-Quipper and discuss open problems.

One perspective on quantum algorithms is that they are classical algorithms having access to a special kind of memory with exotic properties. This perspective suggests that, even in the case of quantum algorithms, the control flow notions of sequencing, conditionals, loops, and recursion are entirely classical. There is however, another notion of control flow, that is itself quantum. The notion of quantum conditional expression is reasonably well-understood: the execution of the two expressions becomes itself a superposition of executions. The quantum counterpart of loops and recursion is however still unclear. In this talk, we argue that, under the right circumstances, a reasonable notion of quantum loops and recursion is possible. To this aim, we first propose a classical, typed, reversible language with lists and fixpoints. We then extend this language to the closed quantum domain (without measurements) by allowing linear combinations of terms and restricting fixpoints to structurally recursive fixpoints whose termination proofs match the proofs of convergence of sequences in infinite-dimensional Hilbert spaces. We additionally give an operational semantics for the quantum language in the spirit of algebraic lambda-calculi.

The talk will be based on arXiv:1804.00952.

Embedded quantum circuit languages like Quipper, LiQUi|⟩, and ProjectQ let programmers express high-level algorithms using host language libraries and features like recursion and data structures. But how can we verify the correctness of embedded quantum circuits without reasoning about the semantics of the entire host language? QWIRE (pronounced “choir”) is a quantum circuit language embedded in Coq, a dependently-typed programming language and interactive theorem prover. QWIRE both has the benefits of an embedded language and can be formally verified inside Coq itself. In this talk I will present the theory and semantics of QWIRE and show how to formally verify the correctness of quantum programs using QWIRE’s denotational semantics.

We will discuss the requirements for programming languages for quantum computers and highlight the differences with programming languages for classical computers. Then we will see how these new requirements are addressed in Q#. This talk will also serve as an introduction to Q#.

Although quantum computing is now a decades-old field, there are still many low-hanging opportunities for improving the projected costs of quantum algorithms by orders of magnitude. For example, when designing an efficient quantum algorithm one can often identify nearly-classical subproblems. Efficient classical circuits for these subproblems translate into efficient quantum circuits for the original algorithm.

This talk will discuss a concrete example of the quantum-to-classical-and-back approach bearing fruit. I will show that preparing a particular type of superposition is equivalent to fitness proportionate selection (a classical task where one has a population of items with associated fitnesses and wishes to sample items with twice as much fitness twice as often). I will then explain an efficient classical algorithm for fitness proportionate selection, and translate it back into the quantum domain to produce the 'subprepare' oracle from arXiv:1805.03662, which prepares (and unprepares) superpositions with hardcoded coefficients 100x more efficiently than previous work.

[joint work with Ankush Das and Jan Hoffmann]

We usually analyze sequential programs in terms of time and space complexity. For concurrent programs, there are richer sets of quantities of interest. For example, in fork/join parallelism we analyze work (that is, the total number of operations) and span (that is, time under the assumption of maximal parallelism). Other measures of interest include latency and throughput of pipelines and response times for interactive systems.

In this talk we show how to extend a system of basic session types for message-passing concurrent processes to capture various aspects of parallel complexity. In particular, we introduce ergometric session types to measure work and temporal session types to measure time. Work and time remain abstract in the sense that we can support different concrete cost models in the same framework. We illustrate our approach via simple examples of message-passing concurrent programs with their types.

Session types can be viewed as arising from a computational interpretation of linear logic where cut reduction in the sequent calculus corresponds to communication. We provide a preliminary assessment of how well ergometric and temporal types fit with this logical foundation.

Session types statically guarantee that communication complies with a protocol. However, most accounts of session typing do not account for failure, which means they are of limited use in real applications---especially distributed applications---where failure is pervasive.

We present the first formal integration of asynchronous session types with exception handling in a functional programming language. We define a core calculus which satisfies preservation and progress properties, is deadlock free, confluent, and terminating.

We provide the first implementation of session types with exception handling for a fully-fledged functional programming language, by extending the Links web programming language; our implementation draws on existing work on algebraic effects and effect handlers.

Session types is a typing discipline for concurrent and distributed processes that allows errors such as communication mismatches and deadlocks to be detected statically. Refinement types are types elaborated by logical constraints that allow richer and finer-grained specification of application properties, combining types with logical formulae that may refer to program values and can constrain types using arbitrary predicates. Type providers, developed in F#, are compile-time components for on-demand code generation. Their architecture relies on an open-compiler, where provider-authors implement a small interface that allows them to inject new names/types into the programming context as the program is written.

In this talk, I will present a library that integrates aspects from the above fields to realise practical applications of multiparty refinement session types (MPST) for any .Net language. Our library supports the specification and validation of distributed message passing protocols based on a formulation of asynchronous MPST enriched with interaction refinements: a collection of features related to the refinement of protocols, such as message-type refinements (value constraints) and value dependent control flow. The combination of these aspects—session types for structured interactions, constraint solving from refinement types, and protocol-specific code generation—enables the specification and implementation of enriched protocols in native F# (and any .Net-compiled language) without requiring language extensions or external pre-processing of user programs. A well-typed endpoint program using our library is guaranteed to perform only compliant session I/O actions w.r.t. to the refined protocol, up to premature termination. The safety guarantees are achieved by a combination of static type checking of the generated types for messages and I/O operations, correctness by construction from code generation, and automated inlining of assertions.

Session types are a typing discipline for message-passing concurrency that enables the specification of communication protocols as channel types, which can then be statically and/or dynamically enforced in order to ensure various correctness properties such as deadlock-freedom and protocol compliance.

However, in most session typing frameworks the language of types (and so, the language of protocols) is kept fairly limited, consisting mainly of sequential descriptions of input and output actions, combined with some form of branching or alternative behaviours.

In this talk I will present a dependent type theory, realised in a concurrent functional language based on the Curry-Howard interpretation of linear logic, that allows for session processes to depend on functions and vice-versa, as well as for the definition of type-level functions. By enriching the type language in this way, we are able to specify protocols where the choice of the next communication action can truly depend on the specific values of exchanged data -- a significant gain in expressiveness wrt the state of the art. I will also show how the type theoretic nature of the framework allows us to internally describe and prove predicates on process behaviours, akin to dependently-typed specifications of functional programs.

Finally, in order to both justify some of our design choices and to benchmark the expressiveness of the theory I will introduce a faithful embedding (up-to the theory's internal equality) of the functional layer of the calculus within the session-typed process layer.

We are entering a magical era, as everything around us becomes responsive and adaptive. To make this happen, it needs to be easy to make computer programs adapt, and the main road we see ahead is differentiable programming: being able to compute and derivatives (primarily gradients) of arbitrary programs. These differentiation operators should be first class: general, robust, performant, and deeply embedded in compilers. I will discuss some subtle difficulties that arise, which have two main causes: approximation, and use of an explicit basis. Both seem unavoidable when building practical systems, and these issues will only become more prominent as our systems grow in complexity.