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

Displayed time zone: Tijuana, Baja California change

16:00 - 18:05
Semantics and SynthesisCoqPL at Watercourt A
Chair(s): Ilya Sergey University College London
16:00
25m
Talk
Phantom Types for Quantum Programs
CoqPL
Robert Rand University of Pennsylvania, Jennifer Paykin University of Pennsylvania, Steve Zdancewic University of Pennsylvania
File Attached
16:25
25m
Talk
Revisiting Parametricity: Inductives and Uniformity of Propositions
CoqPL
Abhishek Anand Cornell University, Greg Morrisett Cornell University
File Attached
16:50
25m
Talk
Towards Context-Aware Data Refinement
CoqPL
Paul Krogmeier Purdue University, Steven Kidd Purdue University, Benjamin Delaware Purdue University
File Attached
17:15
25m
Talk
Mechanizing the Construction and Rewriting of Proper Functions in Coq
CoqPL
Edwin Westbrook Galois, Inc.
File Attached
17:40
25m
Talk
A calculus for logical refinements in separation logic
CoqPL
Dan Frumin Radboud University, Robbert Krebbers Delft University of Technology
File Attached