POPL 2018 (series) / CoqPL 2018 (series) / The Fourth International Workshop on Coq for Programming Languages /
Phantom Types for Quantum Programs
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.
(Rand-al-CoqPL18-Slides.pdf) | 1.35MiB |
(Rand-al-CoqPL18.pdf) | 1.14MiB |
Sat 13 Jan Times are displayed in time zone: Tijuana, Baja California change
Sat 13 Jan
Times are displayed in time zone: Tijuana, Baja California change
16:00 - 18:05: Semantics and SynthesisCoqPL at Watercourt A Chair(s): Ilya SergeyUniversity College London | |||
16:00 - 16:25 Talk | Phantom Types for Quantum Programs CoqPL Robert RandUniversity of Pennsylvania, Jennifer PaykinUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania File Attached | ||
16:25 - 16:50 Talk | Revisiting Parametricity: Inductives and Uniformity of Propositions CoqPL File Attached | ||
16:50 - 17:15 Talk | Towards Context-Aware Data Refinement CoqPL File Attached | ||
17:15 - 17:40 Talk | Mechanizing the Construction and Rewriting of Proper Functions in Coq CoqPL Edwin WestbrookGalois, Inc. File Attached | ||
17:40 - 18:05 Talk | A calculus for logical refinements in separation logic CoqPL File Attached |