Willem Seynaeve
student at Kuleuven
Willem is a student interested in programming languages, type theory, theoretical computer science and mathematics. He is currently pursuing a masters degree in computer science at the KULeuven where he is involved in a research thesis under the supervision of Koen Pauwels and Prof. Tom Schrijvers.
State will do
The main strength of pure languages like Haskell is that they allow a straightforward way of reasoning about programs called equational reasoning. Gibbons and Hinze propose an axiomatic approach for monadic equational reasoning which uses laws to characterise effects. In this paper they show how the state monad and the nondeterminism monad can be combined in one effect called backtrackable state (or “local state”) and they illustrate how the two effects interact. A second way for state and nondeterminism to interact is non-backtrackable state (or “global state”) where state persists after backtracking. Pauwels et al. show how backtrackable state can be simulated with non-backtrackable state and prove correctness using the axiomatic approach proposed by Gibbons and Hinze. Within this project we take this approach one step further and simulate the backtrackable state (state and nondeterminism) with only the state effect.
SlidesVideo ←Back
