To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Interactive programming i… - University of Gothenburg, Sweden Till startsida
Sitemap
To content Read more about how we use cookies on gu.se

Contact form








 


Note! If you want an answer on a question you must specify your email address




Interactive programming in Agda - Objects and graphical user interfaces

Journal article
Authors Andreas Abel
S. Adelsberger
A. Setzer
Published in Journal of Functional Programming
Volume 27
ISSN 0956-7968
Publication year 2017
Published at Department of Computer Science and Engineering (GU)
Language en
Links doi.org/10.1017/s0956796816000319
Keywords recursive definitions, termination, Computer Science
Subject categories Software Engineering, Computer Science

Abstract

We develop a methodology for writing interactive and object-based programs (in the sense of Wegner) in dependently typed functional programming languages. The methodology is implemented in the ooAgda library. ooAgda provides a syntax similar to the one used in object-oriented programming languages, thanks to Agda's copattern matching facility. The library allows for the development of graphical user interfaces (GUIs), including the use of action listeners. Our notion of interactive programs is based on the IO monad defined by Hancock and Setzer, which is a coinductive data type. We use a sized coinductive type which allows us to write corecursive programs in a modular way. Objects are server-side interactive programs that respond to method calls by giving answers and changing their state. We introduce two kinds of objects: simple objects and IO objects. Methods in simple objects are pure, while method calls in IO objects allow for interactions before returning their result. Our approach also allows us to extend interfaces and objects by additional methods. We refine our approach to state-dependent interactive programs and objects through which we can avoid exceptions. For example, with a state-dependent stack object, we can statically disable the pop method for empty stacks. As an example, we develop the implementation of recursive functions using a safe stack. Using a coinductive notion of object bisimilarity, we verify basic correctness properties of stack objects and show the equivalence of different stack implementations. Finally, we give a proof of concept that our interaction model allows to write GUI programs in a natural way: we present a simple drawing program, and a program which allows the users to move a small spaceship using a button.

Page Manager: Webmaster|Last update: 9/11/2012
Share:

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?

Denna text är utskriven från följande webbsida:
http://www.gu.se/english/research/publication/?feedbackForm=true&returnAddress=http%3A%2F%2Fwww.gu.se%2Fenglish%2Fresearch%2Fpublication%2F%3Fprint%3Dtrue%26tipFriend%3Dtrue%26tipUrl%3Dhttp%253A%252F%252Fwww.gu.se%252Fenglish%252Fresearch%252Fpublication%252F%253FpublicationId%253D251637%26publicationId%3D251637&recipientName=Webmaster&encodedEmail=YW5uaWthLmtvbGRlbml1c0BndS5zZQ&tipFriend=true&tipUrl=http%3A%2F%2Fwww.gu.se%2Fenglish%2Fresearch%2Fpublication%2F%3FpublicationId%3D251637&publicationId=251637
Utskriftsdatum: 2019-12-16