Abstract Machine Semantics for Quipper

Colledan, Andrea (2021) Abstract Machine Semantics for Quipper. [Laurea magistrale], Università di Bologna, Corso di Studio in Informatica [LM-DM270]
Documenti full-text disponibili:
[img] Documento PDF (Thesis)
Disponibile con Licenza: Creative Commons: Attribuzione - Condividi allo stesso modo 4.0 (CC BY-SA 4.0)

Download (684kB)

Abstract

Quipper is a domain-specific programming language for the description of quantum circuits. Because it is implemented as an embedded language in Haskell, Quipper is a very practical functional language. However, for the same reason, it lacks a formal semantics and it is limited by Haskell's type-system. In particular, because Haskell lacks linear types, it is easy to write Quipper programs that violate the non-cloning property of quantum states. In order to formalize relevant fragments of Quipper in a type-safe way, the Proto-Quipper family of research languages has been introduced over the last years. In this thesis we first introduce Quipper and Proto-Quipper-M. Proto-Quipper-M is an instance of the Proto-Quipper family based on a categorical model for quantum circuits, which features a linear type-system that guarantees that the non-cloning property holds at compile time. We then derive a tentative small-step operational semantics from the big-step semantics of Proto-Quipper-M and we prove that the two are equivalent. After proving subject reduction and progress results for the tentative semantics, we build upon it to obtain a truly small-step semantics in the style of an abstract machine, which we eventually prove to be equivalent to the original semantics.

Abstract
Tipologia del documento
Tesi di laurea (Laurea magistrale)
Autore della tesi
Colledan, Andrea
Relatore della tesi
Scuola
Corso di studio
Indirizzo
CURRICULUM A: TECNICHE DEL SOFTWARE
Ordinamento Cds
DM270
Parole chiave
Quipper,Proto-Quipper-M,Quantum computing,Quantum programming,Programming languages,Operational semantics,Abstract machines
Data di discussione della Tesi
18 Marzo 2021
URI

Altri metadati

Statistica sui download

Gestione del documento: Visualizza il documento

^