{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:57:21Z","timestamp":1776891441160,"version":"3.51.2"},"reference-count":76,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2017,2,6]],"date-time":"2017-02-06T00:00:00Z","timestamp":1486339200000},"content-version":"unspecified","delay-in-days":36,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2017]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>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.<\/jats:p>\n                  <jats:p>\n                    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\n                    <jats:italic>sized<\/jats:italic>\n                    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.\n                  <\/jats:p>\n                  <jats:p>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.<\/jats:p>","DOI":"10.1017\/s0956796816000319","type":"journal-article","created":{"date-parts":[[2017,2,5]],"date-time":"2017-02-05T23:23:51Z","timestamp":1486337031000},"source":"Crossref","is-referenced-by-count":8,"title":["Interactive programming in Agda \u2013 Objects and graphical user interfaces"],"prefix":"10.46298","volume":"27","author":[{"given":"ANDREAS","family":"ABEL","sequence":"first","affiliation":[]},{"given":"STEPHAN","family":"ADELSBERGER","sequence":"additional","affiliation":[]},{"given":"ANTON","family":"SETZER","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2017,2,6]]},"reference":[{"key":"S0956796816000319_ref65","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0018349"},{"key":"S0956796816000319_ref63","first-page":"454","volume-title":"Proceedings if CSL 2010","author":"Nordvall Forsberg","year":"2010"},{"key":"S0956796816000319_ref38","unstructured":"Granstr\u00f6m J. G. 2016 Intuitionistic Programming Language. Retrieved July 08, 2016. Available at: http:\/\/intuitionistic.org\/"},{"key":"S0956796816000319_ref52","doi-asserted-by":"publisher","DOI":"10.1145\/2976022.2976032"},{"key":"S0956796816000319_ref67","doi-asserted-by":"crossref","unstructured":"Sacchini J. L. (2013) Type-based productivity of stream definitions in the calculus of constructions. In Proceedings of 28th IEEE Symposium on Logic in Computer Science, LICS '13. IEEE Computer Society, pp. 233\u2013242.","DOI":"10.1109\/LICS.2013.29"},{"key":"S0956796816000319_ref45","volume-title":"From Sets and Types to Topology and Analysis. Towards Practicable Foundations for Constructive Mathematics","author":"Hancock","year":"2005"},{"key":"S0956796816000319_ref31","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(02)00096-9"},{"key":"S0956796816000319_ref11","volume-title":"Structure and Interpretation of Computer Programs","author":"Abelson","year":"1996"},{"key":"S0956796816000319_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784732"},{"key":"S0956796816000319_ref54","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1145\/1017472.1017483","volume-title":"Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2004","author":"Leijen","year":"2004"},{"key":"S0956796816000319_ref28","unstructured":"Coq Community. (2015) The Coq Proof Assistant. Available at: https:\/\/coq.inria.fr\/."},{"key":"S0956796816000319_ref21","unstructured":"Bauer A. & Pretnar M. (2012) Programming with algebraic effects and handlers. arXiv http:\/\/arxiv.org\/abs\/1203.1539."},{"key":"S0956796816000319_ref68","doi-asserted-by":"crossref","unstructured":"Sculthorpe N. & Nilsson H. (2009) Safe functional reactive programming through dependent types. In Hutton G. & Tolmach A. P. (eds), Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming, ICFP 2009. ACM, pp. 23\u201334.","DOI":"10.1145\/1596550.1596558"},{"key":"S0956796816000319_ref12","unstructured":"Agda. 2016 With-abstraction. Retrieved November 28, 2016. Available at: http:\/\/agda.readthedocs.io\/en\/latest\/language\/with-abstraction.html"},{"key":"S0956796816000319_ref36","volume-title":"Proceedings of the 6th International Conference on Foundations of Software Science and Computational Structures, FoSSaCS 2003","author":"Gordon","year":"2003"},{"key":"S0956796816000319_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055070"},{"key":"S0956796816000319_ref5","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.43.2"},{"key":"S0956796816000319_ref33","unstructured":"Gim\u00e9nez E. (1996 December) Un calcul de constructions infinies et son application a la v\u00e9rification de syst\u00e8mes communicants (Ph.D. thesis), Ecole Normale Sup\u00e9rieure de Lyon. Th\u00e8se d'universit\u00e9."},{"key":"S0956796816000319_ref16","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.33"},{"key":"S0956796816000319_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"S0956796816000319_ref7","first-page":"1","article-title":"A predicative analysis of structural recursion","volume":"12","author":"Abel","year":"2002","journal-title":"J. Func. Program."},{"key":"S0956796816000319_ref6","doi-asserted-by":"crossref","unstructured":"Abel A. (2012) Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types. In Miller D. & \u00c9sik Z. (eds), Proceedings of the 8th workshop on Fixed Points in Computer Sciience, FICS 2012 Electronic Proceedings in Theoretical Computer Science, vol. 77, pp. 1\u201311. Invited talk.","DOI":"10.4204\/EPTCS.77.1"},{"key":"S0956796816000319_ref71","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29198-7_12"},{"key":"S0956796816000319_ref50","volume-title":"Proceedings of the 23rd ACM Symposium on Principles of Programming Languages, POPL'96","author":"Hughes","year":"1996"},{"key":"S0956796816000319_ref43","first-page":"317","volume-title":"Proceedings of the 14th International Workshop on Computer Science Logic, CSL 2000, 9th Annual Conference of the EACSL","author":"Hancock","year":"2000"},{"key":"S0956796816000319_ref13","unstructured":"Agda Wiki. 2011 MAlonzo. Retrieved October 11, 2016. Available at: http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php?n=Docs.MAlonzo"},{"key":"S0956796816000319_ref76","doi-asserted-by":"publisher","DOI":"10.1145\/38765.38823"},{"key":"S0956796816000319_ref70","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-4435-6_16"},{"key":"S0956796816000319_ref47","unstructured":"Haskell W. 2016 wxHaskell quick start. Retrieved February 09, 2016. Available at: https:\/\/wiki.haskell.org\/WxHaskell\/Quick_start"},{"key":"S0956796816000319_ref46","doi-asserted-by":"publisher","DOI":"10.1145\/1378704.1378725"},{"key":"S0956796816000319_ref60","first-page":"249","volume-title":"Proceedings of the 1st IEEE Symposium on Logic in Computer Science, LICS '86","author":"Mendler","year":"1986"},{"key":"S0956796816000319_ref53","first-page":"228","volume-title":"Proceedings of the 15th International Symposium on Practical Aspects of Declarative Languages, PADL 2013","author":"Jeffrey","year":"2013"},{"key":"S0956796816000319_ref25","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/978-3-540-25979-4_2","volume-title":"Rewriting Techniques and Applications, RTA 2004","author":"Blanqui","year":"2004"},{"key":"S0956796816000319_ref4","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(2:3)2008"},{"key":"S0956796816000319_ref41","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2005.05.022"},{"key":"S0956796816000319_ref51","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014058"},{"key":"S0956796816000319_ref35","unstructured":"Girard J.-Y. (1972) Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieur (Th\u00e8se de Doctorat d'\u00c9tat). Universit\u00e9 de Paris VII."},{"key":"S0956796816000319_ref39","unstructured":"Hackage. 2016 Control.Monad.STM. Retrieved February 17, 2016. Available at: https:\/\/hackage.haskell.org\/package\/stm-2.4.4\/docs\/Control-Monad-STM.html"},{"key":"S0956796816000319_ref59","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"S0956796816000319_ref40","first-page":"629","article-title":"Codatatypes in ML","volume":"8","author":"Hagino","year":"1989","journal-title":"J. Symb. Logic"},{"key":"S0956796816000319_ref73","volume-title":"Proceedings of the 6th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2003","author":"Sprenger","year":"2003"},{"key":"S0956796816000319_ref19","first-page":"71","volume-title":"Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications, TLCA 2005","author":"Barthe","year":"2005"},{"key":"S0956796816000319_ref37","doi-asserted-by":"publisher","DOI":"10.4304\/jsw.7.5.1136-1148"},{"key":"S0956796816000319_ref75","doi-asserted-by":"publisher","DOI":"10.1145\/2841316"},{"key":"S0956796816000319_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053541"},{"key":"S0956796816000319_ref3","first-page":"286","volume-title":"Proceedings of the 5th Asian Symposium on Programming Languages and Systems, APLAS 2007","author":"Abel","year":"2007"},{"key":"S0956796816000319_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38946-7_13"},{"key":"S0956796816000319_ref23","unstructured":"Benke M. (2007) Alonzo \u2013 A compiler for Agda. Talk given at TYPES 2007. Available at: http:\/\/www.mimuw.edu.pl\/ben\/Papers\/TYPES07-alonzo.pdf"},{"key":"S0956796816000319_ref10","unstructured":"Abel A. , Adelsberger S. & Setzer A. (2016) ooAgda. Available at: https:\/\/github.com\/agda\/ooAgda"},{"key":"S0956796816000319_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500591"},{"key":"S0956796816000319_ref18","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129503004122"},{"key":"S0956796816000319_ref27","first-page":"18","volume-title":"Proceedings of the 15th International Symposium on Trends in Functional Programming, TFP 2014","author":"Brady","year":"2014"},{"key":"S0956796816000319_ref69","first-page":"91","volume-title":"Revised Selected Papers from the 7th Symposium on Trends in Functional Programming, TFP 2006","author":"Setzer","year":"2006"},{"key":"S0956796816000319_ref55","unstructured":"Leijen D. 2015 (Commit f2f5b5a 23 September) wxAsteroids. Available at: https:\/\/github.com\/wxHaskell\/wxAsteroids"},{"key":"S0956796816000319_ref62","volume-title":"Handbook of Logic in Computer Science: Logic and Algebraic Methods","author":"Nordstr\u00f6m","year":"2001"},{"key":"S0956796816000319_ref58","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020831825964"},{"key":"S0956796816000319_ref61","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"S0956796816000319_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"S0956796816000319_ref72","volume-title":"Dependently Typed Programming 2004","author":"Setzer","year":"2004"},{"key":"S0956796816000319_ref66","volume-title":"Proceedings of the 23rd ACM Symposium on Principles of Programming Languages, POPL'96","author":"Peyton","year":"1996"},{"key":"S0956796816000319_ref49","unstructured":"Hudak P. 2016 SOE library. Retrieved February 12, 2016. Available at: http:\/\/www.cs.yale.edu\/homes\/hudak\/SOE\/software1.htm"},{"key":"S0956796816000319_ref44","unstructured":"Hancock P. & Setzer A. (2000b) Specifying interactions with dependent types. In Proceedings of the Workshop on Subtyping and Dependent Types in Programming, Portugal, 7 July 2000. Electronic proceedings, available at: http:\/\/www-sop.inria.fr\/oasis\/DTP00\/Proceedings\/proceedings.html"},{"key":"S0956796816000319_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8598-9"},{"key":"S0956796816000319_ref20","first-page":"493","volume-title":"Proceedings of the 22nd International Workshop on Computer Science Logic, CSL 2008, 17th Annual Conference of the EACSL","author":"Barthe","year":"2008"},{"key":"S0956796816000319_ref15","unstructured":"Altenkirch T. & Danielsson N. A. (2012) Termination checking in the presence of nested inductive and coinductive types. In Bove A. , Komendantskaya E. & Niqui M. (eds), Proceedings of the workshop on Partiality And Recursion in Interactive Theorem Provers, PAR 2010 EPiC Series in Computer Science, vol. 5. EasyChair, pp. 101\u2013106."},{"key":"S0956796816000319_ref26","unstructured":"Boehm H.-J. & Steele G. L. Jr. (eds). (1996) In Proceedings of the 23rd ACM Symposium on Principles of Programming Languages, POPL'96. ACM."},{"key":"S0956796816000319_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58085-9_72"},{"key":"S0956796816000319_ref74","doi-asserted-by":"crossref","unstructured":"Strom R. E. & Yemini S. (1986) Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Softw. Eng., 157\u2013171.","DOI":"10.1109\/TSE.1986.6312929"},{"key":"S0956796816000319_ref9","first-page":"27","volume-title":"Proceedings of the 40th ACM Symposium on Principles of Programming Languages, POPL 2013","author":"Abel","year":"2013"},{"key":"S0956796816000319_ref32","doi-asserted-by":"publisher","DOI":"10.1145\/2629609"},{"key":"S0956796816000319_ref2","volume-title":"Proceedings of the International Conference on Foundations of Software Science and Computation Structure, FOSSACS 2003","author":"Abbott","year":"2003"},{"key":"S0956796816000319_ref48","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2008.7.3.a4"},{"key":"S0956796816000319_ref14","unstructured":"Agda Wiki. (2016) The Agda Wiki. Available at: http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php"},{"key":"S0956796816000319_ref64","unstructured":"Norell U. (2007 September) Towards a Practical Programming Language Based on Dependent Type Theory (Ph.D. thesis). G\u00f6teborg, Sweden: Dept. of Comput. Sci. and Eng., Chalmers Univ."},{"key":"S0956796816000319_ref57","volume-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"S0956796816000319_ref56","unstructured":"Lochbihler A. & Z\u00fcst M. (2014) Programming TLS in Isabelle\/HOL. In Proceedings of Isabelle Workshop, Associated with ITP 2014. Available from https:\/\/www.ethz.ch\/content\/dam\/ethz\/special-interest\/infk\/inst-infsec\/information-security-group-dam\/people\/andreloc\/lochbihler14iw.pdf."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796816000319","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:19:53Z","timestamp":1776889193000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796816000319\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"references-count":76,"alternative-id":["S0956796816000319"],"URL":"https:\/\/doi.org\/10.1017\/s0956796816000319","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"article-number":"e8"}}