log in  |  register  |  feedback?  |  help  |  web accessibility
Logo
Linear dependent types for quantum circuit programming
Monday, February 17, 2020, 12:00-1:00 pm Calendar
  • You are subscribed to this talk through .
  • You are watching this talk through .
  • You are subscribed to this talk. (unsubscribe, watch)
  • You are watching this talk. (unwatch, subscribe)
  • You are not subscribed to this talk. (watch, subscribe)
Abstract

It is sometimes said that 99% of a quantum programmer's task is constructing and manipulating circuits and only 1% is actually running them. In this talk, I will introduce and demonstrate Proto-Quipper-D, an experimental quantum circuit programming language. Like previous versions of Proto-Quipper, it uses linear types to enforce the no-cloning property. In addition, Proto-Quipper-D features the use of dependent types for describing families of circuits and for type-safe garbage qubit management.

Bio

Frank Fu is a postdoctoral researcher in the Department of Mathematics and Statistics at Dalhousie University. Broadly speaking, he is interested in type theories and their applications in programming languages. In the past, he worked on supporting the verification of lambda-encoded programs in a type system and in a higher-order logic, and has explored topics relating to Haskell-style type classes, term rewriting, nested data types, and dependent types. Currently, he is working on the design and implementation of a linear dependently typed programming language for circuit design.

This talk is organized by Mike Hicks