Sat 13 Jan 2018 16:00 - 16:25 at Watercourt A - Semantics and Synthesis Chair(s): Ilya Sergey

We explore the design space of using dependent types to type check and verify quantum circuits. We weigh the trade-offs between the expressivity of dependent types against the costs imposed by large proof terms. We propose lightweight dependent types, or phantom types, as a middle ground, which provide useful type information for programming while specifying the properties to be externally verified.