A Formal Foundation for Variational Programming Using the Choice Calculus

Graduate Thesis Or Dissertation

Pubblico Deposited

Citeable URL: https://ir.library.oregonstate.edu/concern/graduate_thesis_or_dissertations/8p58ph92j

Descriptions

Attribute Name	Values
Creator	Hubbard, Spencer
Abstract	In this thesis, we present semantic equivalence rules for an extension of the choice calculus and sound operations for an implementation of variational lists. The choice calculus is a calculus for describing variation and the formula choice calculus is an extension with formulas. We prove semantic equivalence rules for the formula choice calculus. Variational lists are functional data structures for representing and computing with variation in lists using the choice calculus. We prove map and bind operations are sound for an implementation of variational lists. These proofs are written and verified in the language of the Coq proof assistant.
License	All rights reserved
Resource Type	Masters Thesis
Date Available	2016-06-23T17:09:00+00:00
Date Issued	2016-06-01
Degree Level	Master's
Degree Name	Master of Science (M.S.)
Degree Field	Computer Science
Degree Grantor	Oregon State University
Commencement Year	2016
Advisor	Walkingshaw, Eric
Committee Member	Erwig, Martin Niess, Maggie Redfield, Stephen
Academic Affiliation	Electrical Engineering and Computer Science
Non-Academic Affiliation	Oregon State University. Graduate School
Subject	Calculus of variations
Dichiarazione dei diritti	In Copyright
Publisher	Oregon State University
Peer Reviewed	No
Language	English [eng]
Replaces	http://hdl.handle.net/1957/59312

Parents:

This work has no parents.

In Collection:

Thumbnail	Titolo	Data caricata	Visibilità	Azioni
	HubbardSpencerM2016.pdf	2017-08-22	Pubblico	Scaricare