Q*: Implementing Quantum Separation Logic in F* (PLanQC 2022)

Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia

Who

Kesha Hietala, Sarah Marshall, Robert Rand, Nikhil Swamy

Track

PLanQC 2022

Time Zone

The program is currently displayed in (GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague.

Use conference time zone: (GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, PragueSelect 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

Thu 15 Sep 2022 15:05 - 15:30 at E3 - Formalization, verification, and correctness Chair(s): Ross Duncan

Abstract

In this extended abstract we present ongoing work on implementing a quantum separation logic in F* and discuss our prototype implementation of a proof of correctness for teleport with entanglement.

File attachments

abstract (planqc2022-paper84.pdf)	503KiB

Kesha Hietala

University of Maryland

United States

Sarah Marshall

Microsoft Quantum

Robert Rand

University of Chicago

United States

Nikhil Swamy

MSR Redmond

United States

Time Zone

The program is currently displayed in (GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague.

Use conference time zone: (GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, PragueSelect 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

Thu 15 Sep
Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change

14:00 - 15:30	Formalization, verification, and correctnessPLanQC at E3 Chair(s): Ross Duncan Cambridge Quantum Computing

14:00 40m Talk		Invited talk: Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs PLanQC Charles Yuan MIT CSAIL
14:40 25m Talk		Analyzing quantum programs using the power of interaction PLanQC Agnes Villanyi MIT, Charles Yuan MIT CSAIL, Christopher McNally MIT RLE File Attached
15:05 25m Talk		Q: Implementing Quantum Separation Logic in F PLanQC Kesha Hietala University of Maryland, Sarah Marshall Microsoft Quantum, Robert Rand University of Chicago, Nikhil Swamy MSR Redmond File Attached