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.

Sat 13 Jan

CoqPL-2018
16:00 - 18:05: - Semantics and Synthesis at Watercourt A
Chair(s): Ilya SergeyUniversity College London
CoqPL-2018151585560000016:00 - 16:25
Talk
Robert RandUniversity of Pennsylvania, Jennifer PaykinUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
File Attached
CoqPL-2018151585710000016:25 - 16:50
Talk
Abhishek AnandCornell University, Greg MorrisettCornell University
File Attached
CoqPL-2018151585860000016:50 - 17:15
Talk
Paul KrogmeierPurdue University, Steven KiddPurdue University, Benjamin DelawarePurdue University
File Attached
CoqPL-2018151586010000017:15 - 17:40
Talk
Edwin WestbrookGalois, Inc.
File Attached
CoqPL-2018151586160000017:40 - 18:05
Talk
Dan FruminRadboud University, Robbert KrebbersDelft University of Technology
File Attached