Towards Reasoning about State Transformer Monads in Agda

Examensarbete för masterexamen

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12380/117330
Download file(s):
File Description SizeFormat 
117330.pdfFulltext784.11 kBAdobe PDFView/Open
Type: Examensarbete för masterexamen
Master Thesis
Title: Towards Reasoning about State Transformer Monads in Agda
Authors: Bui, Viet Ha
Abstract: Wouter 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.
Keywords: Datalogi;Programvaruteknik;Computer science;Software Engineering
Issue Date: 2009
Publisher: Chalmers tekniska högskola / Institutionen för data- och informationsteknik, Datavetenskap (Chalmers)
Chalmers University of Technology / Department of Computer Science and Engineering, Computing Science (Chalmers)
URI: https://hdl.handle.net/20.500.12380/117330
Collection:Examensarbeten för masterexamen // Master Theses



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.