A Metalanguage for Guarded Iteration

  • Sergey GoncharovEmail author
  • Christoph Rauch
  • Lutz Schröder
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11187)


Notions of guardedness serve to delineate admissible recursive definitions in various settings in a compositional manner. In recent work, we have introduced an axiomatic notion of guardedness in symmetric monoidal categories, which serves as a unifying framework for various examples from program semantics, process algebra, and beyond. In the present paper, we propose a generic metalanguage for guarded iteration based on combining this notion with the fine-grain call-by-value paradigm, which we intend as a unifying programming language for guarded and unguarded iteration in the presence of computational effects. We give a generic (categorical) semantics of this language over a suitable class of strong monads supporting guarded iteration, and show it to be in touch with the standard operational behaviour of iteration by giving a concrete big-step operational semantics for a certain specific instance of the metalanguage and establishing adequacy for this case.


  1. 1.
    Abramsky, S.: Intensionality, definability and computation. In: Baltag, A., Smets, S. (eds.) Johan van Benthem on Logic and Information Dynamics, pp. 121–142. Springer, Cham (2014). Scholar
  2. 2.
    Appel, A.W., Melliès, P.A., Richards, C.D., Vouillon, J.: A very modal model of a modern, major, general type system. In: Proceedings of 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL 2007, January 2007, Nice, pp. 109–122. ACM Press, New York (2007).
  3. 3.
    Benton, N., Kennedy, A.: Exceptional syntax. J. Funct. Program. 11(4), 395–410 (2001). Scholar
  4. 4.
    Bergstra, J., Ponse, A., Smolka, S. (eds.): Handbook of Process Algebra. Elsevier, New York City (2001). Scholar
  5. 5.
    Birkedal, L., Møgelberg, R., Schwinghammer, J., Støvring, K.: First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Log. Methods Comput. Sci. 8(4), 1 (2012). Scholar
  6. 6.
    Bloom, S., Ésik, Z.: Iteration Theories: The Equational Logic of Iterative Processes. EATCS Monographs on Theoretical Computer Science. Springer, Heidelberg (1993). Scholar
  7. 7.
    Brookes, S., Van Stone, K.: Monads and comonads in intensional semantics. Technical report CMU-CS-93-140, Department of Computer Science, Carnegie-Mellon University, Pittsburgh, PA (1993)Google Scholar
  8. 8.
    Carboni, A., Lack, S., Walters, R.: Introduction to extensive and distributive categories. J. Pure. Appl. Algebra 84, 145–158 (1993). Scholar
  9. 9.
    Clouston, R., Bizjak, A., Grathwohl, H.B., Birkedal, L.: The guarded lambda-calculus: programming and reasoning with guarded recursion for coinductive types. Log. Methods Comput. Sci. 12(3), 7 (2016). Scholar
  10. 10.
    Cockett, J.R.B.: Introduction to distributive categories. Math. Struct. Comput. Sci. 3(3), 277–307 (1993). Scholar
  11. 11.
    Coquand, T.: Infinite objects in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 62–78. Springer, Heidelberg (1994). Scholar
  12. 12.
    Escardó, M.: A metric model of PCF. Paper Presented at Workshop on Realizability Semantics and Applications, June–July 1999, Trento (1999).
  13. 13.
    Geron, B., Levy, P.B.: Iteration and labelled iteration. Electron. Notes Theor. Comput. Sci. 325, 127–146 (2016). Scholar
  14. 14.
    Giménez, E.: Codifying guarded definitions with recursive schemes. In: Dybjer, P., Nordström, B., Smith, J. (eds.) TYPES 1994. LNCS, vol. 996, pp. 39–59. Springer, Heidelberg (1995). Scholar
  15. 15.
    Giménez, E.: Structural recursive definitions in type theory. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 397–408. Springer, Heidelberg (1998). Scholar
  16. 16.
    Goncharov, S., Milius, S., Rauch, C.: Complete Elgot monads and coalgebraic resumptions. Electron. Notes Theor. Comput. Sci. 325, 147–168 (2016). Scholar
  17. 17.
    Goncharov, S., Rauch, C., Schröder, L.: Unguarded recursion on coinductive resumptions. Electron. Notes Theor. Comput. Sci. 319, 183–198 (2015). Scholar
  18. 18.
    Goncharov, S., Schröder, L.: Guarded traced categories. In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 313–330. Springer, Cham (2018). Scholar
  19. 19.
    Goncharov, S., Schröder, L., Rauch, C., Piróg, M.: Unifying guarded and unguarded iteration. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 517–533. Springer, Heidelberg (2017). Scholar
  20. 20.
    Hancock, P., Setzer, A.: Guarded induction and weakly final coalgebras in dependent type theory. In: Crosilla, L., Schuster, P. (eds.) From Sets and Types to Topology and Analysis. Towards Practicable Foundations for Constructive Mathematics. Oxford Logic Guides, vol. 48, pp. 115–134. Clarendon Press, Oxford (2005)Google Scholar
  21. 21.
    Hyland, M., Plotkin, G., Power, J.: Combining effects: sum and tensor. Theor. Comput. Sci. 357(1–3), 70–99 (2006). Scholar
  22. 22.
    Jones, S.P., et al.: Haskell 98: a non-strict, purely functional language (1999)Google Scholar
  23. 23.
    Krishnaswami, K., Benton, N.: Ultrametric semantics of reactive programs. In: Proceedings of 26th Annual IEEE Symposium on Logic in Computer Science. LICS 2011, June 2011, Toronto, ON, pp. 257–266. IEEE CS Press, Washington, DC (2011).
  24. 24.
    Levy, P.B., Power, J., Thielecke, H.: Modelling environments in call-by-value programming languages. Inf. Comput. 185(2), 182–210 (2003). Scholar
  25. 25.
    Mac Lane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5. Springer, New York (1971). Scholar
  26. 26.
    Milius, S.: Completely iterative algebras and completely iterative monads. Inf. Comput. 196(1), 1–41 (2005). Scholar
  27. 27.
    Milner, R.: Communication and Concurrency. Prentice-Hall, Upper Saddle River (1989)zbMATHGoogle Scholar
  28. 28.
    Moggi, E.: A modular approach to denotational semantics. In: Pitt, D.H., Curien, P.-L., Abramsky, S., Pitts, A.M., Poigné, A., Rydeheard, D.E. (eds.) CTCS 1991. LNCS, vol. 530, pp. 138–139. Springer, Heidelberg (1991). Scholar
  29. 29.
    Nakano, H.: A modality for recursion. In: Proceedings of 15th Annual IEEE Symposium on Logic in Computer Science. LICS 2000, June 2000, Santa Barbara, CA, pp. 255–266. IEEE CS Press, Washington, DC (2000).
  30. 30.
    Nakata, K.: Resumption-based big-step and small-step interpreters for While with interactive I/O. In: Danvy, O., Shan, C. (eds.) Proceedings of IFIP Working Conference on Domain-Specific Languages. DSL 2011, Electronic Proceedings in Theoretical Computer Science, September 2011, Bordeaux, vol. 66, pp. 226–235. Open Publishing Association, Sydney (2011). Scholar
  31. 31.
    Nakata, K., Uustalu, T.: A Hoare logic for the coinductive trace-based big-step semantics of While. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 488–506. Springer, Heidelberg (2010). Scholar
  32. 32.
    Nakata, K., Uustalu, T.: Resumptions, weak bisimilarity and big-step semantics for While with interactive I/O: an exercise in mixed induction-coinduction. In: Aceto, L., Sobocinski, P. (eds.) Proceedings of 7th Workshop on Structural Operational Semantics. SOS 2010, Electronic Proceedings in Theoretical Computer Science, August 2010, Paris. vol. 32, pp. 57–75. Open Publishing Association, Sydney (2010). Scholar
  33. 33.
    Nakata, K., Uustalu, T.: A Hoare logic for the coinductive trace-based big-step semantics of While. Log. Methods Comput. Sci. 11(1), 1 (2015). Scholar
  34. 34.
    Plotkin, G., Power, J.: Adequacy for algebraic effects. In: Honsell, F., Miculan, M. (eds.) FoSSaCS 2001. LNCS, vol. 2030, pp. 1–24. Springer, Heidelberg (2001). Scholar
  35. 35.
    Tait, W.W.: Intensional interpretations of functionals of finite type I. J. Symb. Log. 32(2), 198–212 (1967). Scholar
  36. 36.
    Turi, D., Plotkin, G.: Towards a mathematical operational semantics. In: Proceedings of 12th Annual IEEE Symposium on Logic in Computer Science. LICS 1997, June–July 1997, Warsaw, pp. 280–291. IEEE CS Press, Washington, DC (1997).
  37. 37.
    Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)zbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Sergey Goncharov
    • 1
    Email author
  • Christoph Rauch
    • 1
  • Lutz Schröder
    • 1
  1. 1.Dept. InformatikFriedrich-Alexander-Universität Erlangen-NürnbergErlangenGermany

Personalised recommendations