一句话：提出 Agda 中基于共归纳 IO 与 copattern 匹配的交互式对象编程方法，实现 ooAgda 库并支持 GUI 与对象验证。
论文研究如何在依赖类型函数式语言 Agda 中编写交互式、面向对象的程序。作者提出一套方法并在 ooAgda 库中实现：借助 copattern 匹配提供类似面向对象语言的语法；交互程序基于共归纳 IO monad，并采用 sized coinductive 类型以模块化方式编写核心递归程序。对象是服务端交互程序，分简单对象与 IO 对象，方法可纯或含交互，并支持接口与对象扩展。作者还引入状态依赖交互程序和对象以静态避免异常，例如空栈禁用 pop。最后用共归纳对象互模拟验证栈对象正确性并证明不同栈实现等价，并以绘图程序和按钮控制飞船的 GUI 示例作概念验证。
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.
@article{AbelAS17,
title = {Interactive programming in Agda – Objects and graphical user interfaces},
author = {ANDREAS ABEL and STEPHAN ADELSBERGER and ANTON SETZER},
journal = {Journal of Functional Programming},
volume = {27},
year = {2017},
doi = {10.1017/s0956796816000319}
}