Phantom Types for Quantum Programs (CoqPL 2018 - The Fourth International Workshop on Coq for Programming Languages)

Sun 7 - Sat 13 January 2018 Los Angeles, California, United States

Who

Robert Rand, Jennifer Paykin, Steve Zdancewic

Track

CoqPL 2018

Time Zone

The program is currently displayed in (GMT-08:00) Tijuana, Baja California.

Use conference time zone: (GMT-08:00) Tijuana, Baja CaliforniaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

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

Abstract

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.

File attachments

(Rand-al-CoqPL18-Slides.pdf)	1.35MiB
(Rand-al-CoqPL18.pdf)	1.14MiB

Robert Rand

University of Pennsylvania

United States

Jennifer Paykin

University of Pennsylvania

United States

Steve Zdancewic

University of Pennsylvania

United States

Time Zone

The program is currently displayed in (GMT-08:00) Tijuana, Baja California.

Use conference time zone: (GMT-08:00) Tijuana, Baja CaliforniaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

Display full programSpecify a time band

Save

Session Program

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 Abhishek AnandCornell University, Greg MorrisettCornell University File Attached
	16:50 - 17:15 Talk		Towards Context-Aware Data Refinement CoqPL Paul KrogmeierPurdue University, Steven KiddPurdue University, Benjamin DelawarePurdue University 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 Dan FruminRadboud University, Robbert KrebbersDelft University of Technology File Attached