Till sidans topp

Sidansvarig: Webbredaktion
Sidan uppdaterades: 2012-09-11 15:12

Tipsa en vän
Utskriftsversion

Interactive programming i… - Göteborgs universitet Till startsida
Webbkarta
Till innehåll Läs mer om hur kakor används på gu.se

Interactive programming in Agda - Objects and graphical user interfaces

Artikel i vetenskaplig tidskrift
Författare Andreas Abel
S. Adelsberger
A. Setzer
Publicerad i Journal of Functional Programming
Volym 27
ISSN 0956-7968
Publiceringsår 2017
Publicerad vid Institutionen för data- och informationsteknik (GU)
Språk en
Länkar doi.org/10.1017/s0956796816000319
Ämnesord recursive definitions, termination, Computer Science
Ämneskategorier Programvaruteknik, Datavetenskap (datalogi)

Sammanfattning

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.

Sidansvarig: Webbredaktion|Sidan uppdaterades: 2012-09-11
Dela:

På Göteborgs universitet använder vi kakor (cookies) för att webbplatsen ska fungera på ett bra sätt för dig. Genom att surfa vidare godkänner du att vi använder kakor.  Vad är kakor?

Denna text är utskriven från följande webbsida:
http://www.gu.se/forskning/publikation/?languageId=100000&disableRedirect=true&returnUrl=http%3A%2F%2Fwww.gu.se%2Fenglish%2Fresearch%2Fpublication%2F%3Fprint%3Dtrue%26publicationId%3D251637&publicationId=251637
Utskriftsdatum: 2019-12-16