Towards a formally verified functional quantum programming language

by Green, Alexander S.

Type Thesis
Rate 0.0 /5

This thesis looks at the development of a framework for a functional quantum programming language. The framework is first developed in Haskell, looking at how a monadic structure can be used to explicitly deal with the side-effects inherent in the measurement of quantum systems, and goes on to look at how a dependently-typed reimplementation in Agda gives us the basis for a formally verified quantum programming language. The two implementations are not in themselves fully developed quantum prog…

Read More ↓

Summary

This thesis looks at the development of a framework for a functional quantum programming language. The framework is first developed in Haskell, looking at how a monadic structure can be used to explicitly deal with the side-effects inherent in the measurement of quantum systems, and goes on to look at how a dependently-typed reimplementation in Agda gives us the basis for a formally verified quantum programming language. The two implementations are not in themselves fully developed quantum programming languages, as they are embedded in their respective parent languages, but are a major step towards the development of a full formally verified, functional quantum programming language. Dubbed the “Quantum IO Monad”, this framework is designed following a structural approach as given by a categorical model of quantum computation.

Read More ↓

Edition Statements

  • Publication Date:2010

Thesis Information

  • Degree:Ph.D.
  • University:University of Nottingham

Publication Statements

  • Language:eng
  • Publication Date:2010

Edition Identifiers

  • ethos:523066

Subjects

Writers

Rate & Review

0.0/5
(0 people Voted)

No reviews yet. Be the first to rate this work.

Files & Downloads