Towards a formally verified functional quantum programming language
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...
| Main Author: | |
|---|---|
| Format: | Thesis (University of Nottingham only) |
| Language: | English |
| Published: |
2010
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/11457/ |
| _version_ | 1848791281704108032 |
|---|---|
| author | Green, Alexander S. |
| author_facet | Green, Alexander S. |
| author_sort | Green, Alexander S. |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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. |
| first_indexed | 2025-11-14T18:26:01Z |
| format | Thesis (University of Nottingham only) |
| id | nottingham-11457 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-14T18:26:01Z |
| publishDate | 2010 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-114572025-02-28T11:13:36Z https://eprints.nottingham.ac.uk/11457/ Towards a formally verified functional quantum programming language Green, Alexander S. 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. 2010-07-20 Thesis (University of Nottingham only) NonPeerReviewed application/pdf en arr https://eprints.nottingham.ac.uk/11457/1/thesis.pdf Green, Alexander S. (2010) Towards a formally verified functional quantum programming language. PhD thesis, University of Nottingham. quantum programming computer programming computer languages haskell monadic structure quantum io monad |
| spellingShingle | quantum programming computer programming computer languages haskell monadic structure quantum io monad Green, Alexander S. Towards a formally verified functional quantum programming language |
| title | Towards a formally verified functional quantum programming language |
| title_full | Towards a formally verified functional quantum programming language |
| title_fullStr | Towards a formally verified functional quantum programming language |
| title_full_unstemmed | Towards a formally verified functional quantum programming language |
| title_short | Towards a formally verified functional quantum programming language |
| title_sort | towards a formally verified functional quantum programming language |
| topic | quantum programming computer programming computer languages haskell monadic structure quantum io monad |
| url | https://eprints.nottingham.ac.uk/11457/ |