Towards Reasoning about State Transformer Monads in Agda

Visa enkel post
dc.contributor.authorBui, Viet Ha
dc.contributor.departmentChalmers tekniska högskola / Institutionen för data- och informationsteknik, Datavetenskap (Chalmers)sv
dc.contributor.departmentChalmers University of Technology / Department of Computer Science and Engineering, Computing Science (Chalmers)en
dc.date.accessioned2019-07-03T12:17:43Z
dc.date.available2019-07-03T12:17:43Z
dc.date.issued2009
dc.description.abstractWouter Swierstra showed in his PhD thesis how to implement stateful computations in the dependently typed functional programming language Agda. In particular he defined a notion of state which is parameterized by a list of types indicating what kind of data are to be stored in the respective locations. He also showed how to define monadic state transformation over this notion of state. In this thesis we extend Swierstra’s work with two new contributions. The first is to implement a stateful version of Dijkstra’s algorithm for the Dutch National Flag in Agda. We prove some properties of a function which swaps the contents of two locations, an important step towards showing full correctness of the algorithm in Agda. The second contribution is to formally prove (in Agda) some properties about monads suggested by Plotkin and Power.
dc.identifier.urihttps://hdl.handle.net/20.500.12380/117330
dc.language.isoeng
dc.setspec.uppsokTechnology
dc.subjectDatalogi
dc.subjectProgramvaruteknik
dc.subjectComputer science
dc.subjectSoftware Engineering
dc.titleTowards Reasoning about State Transformer Monads in Agda
dc.type.degreeExamensarbete för masterexamensv
dc.type.degreeMaster Thesisen
dc.type.uppsokH
local.programmeComputer science – algorithms, languages and logic (MPALG), MSc
Ladda ner
Original bundle
Visar 1 - 1 av 1
Bild (thumbnail)
Namn:
117330.pdf
Storlek:
784.11 KB
Format:
Adobe Portable Document Format
Beskrivning:
Fulltext
Ladda ner
Samling
Examensarbeten för masterexamen