Skip to main content
SpringerLink
Log in

A Metalanguage for Guarded Iteration

  • Conference paper
  • First Online:
Book cover Theoretical Aspects of Computing – ICTAC 2018 (ICTAC 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11187))

Included in the following conference series:

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  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). https://doi.org/10.1007/978-3-319-06025-5_5

    Chapter  Google Scholar 

  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). https://doi.org/10.1145/1190216.1190235

  3. Benton, N., Kennedy, A.: Exceptional syntax. J. Funct. Program. 11(4), 395–410 (2001). https://doi.org/10.1017/s0956796801004099

    Article  MathSciNet  MATH  Google Scholar 

  4. Bergstra, J., Ponse, A., Smolka, S. (eds.): Handbook of Process Algebra. Elsevier, New York City (2001). https://doi.org/10.1016/b978-0-444-82830-9.x5017-6

    Book  MATH  Google Scholar 

  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). https://doi.org/10.2168/lmcs-8(4:1)2012

    Article  MathSciNet  MATH  Google Scholar 

  6. Bloom, S., Ésik, Z.: Iteration Theories: The Equational Logic of Iterative Processes. EATCS Monographs on Theoretical Computer Science. Springer, Heidelberg (1993). https://doi.org/10.1007/978-3-642-78034-9

    Book  MATH  Google Scholar 

  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. Carboni, A., Lack, S., Walters, R.: Introduction to extensive and distributive categories. J. Pure. Appl. Algebra 84, 145–158 (1993). https://doi.org/10.1016/0022-4049(93)90035-r

    Article  MathSciNet  MATH  Google Scholar 

  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). https://doi.org/10.2168/lmcs-12(3:7)2016

    Article  MathSciNet  MATH  Google Scholar 

  10. Cockett, J.R.B.: Introduction to distributive categories. Math. Struct. Comput. Sci. 3(3), 277–307 (1993). https://doi.org/10.1017/s0960129500000232

    Article  MathSciNet  MATH  Google Scholar 

  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). https://doi.org/10.1007/3-540-58085-9_72

    Chapter  Google Scholar 

  12. Escardó, M.: A metric model of PCF. Paper Presented at Workshop on Realizability Semantics and Applications, June–July 1999, Trento (1999). http://www.cs.bham.ac.uk/~mhe/papers/metricpcf.pdf

  13. Geron, B., Levy, P.B.: Iteration and labelled iteration. Electron. Notes Theor. Comput. Sci. 325, 127–146 (2016). https://doi.org/10.1016/j.entcs.2016.09.035

    Article  MathSciNet  MATH  Google Scholar 

  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). https://doi.org/10.1007/3-540-60579-7_3

    Chapter  Google Scholar 

  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). https://doi.org/10.1007/BFb0055070

    Chapter  Google Scholar 

  16. Goncharov, S., Milius, S., Rauch, C.: Complete Elgot monads and coalgebraic resumptions. Electron. Notes Theor. Comput. Sci. 325, 147–168 (2016). https://doi.org/10.1016/j.entcs.2016.09.036

    Article  MathSciNet  MATH  Google Scholar 

  17. Goncharov, S., Rauch, C., Schröder, L.: Unguarded recursion on coinductive resumptions. Electron. Notes Theor. Comput. Sci. 319, 183–198 (2015). https://doi.org/10.1016/j.entcs.2015.12.012

    Article  MathSciNet  MATH  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-89366-2_17

    Chapter  Google Scholar 

  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). https://doi.org/10.1007/978-3-662-54458-7_30

    Chapter  MATH  Google Scholar 

  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. Hyland, M., Plotkin, G., Power, J.: Combining effects: sum and tensor. Theor. Comput. Sci. 357(1–3), 70–99 (2006). https://doi.org/10.1016/j.tcs.2006.03.013

    Article  MathSciNet  MATH  Google Scholar 

  22. Jones, S.P., et al.: Haskell 98: a non-strict, purely functional language (1999)

    Google Scholar 

  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). https://doi.org/10.1109/lics.2011.38

  24. Levy, P.B., Power, J., Thielecke, H.: Modelling environments in call-by-value programming languages. Inf. Comput. 185(2), 182–210 (2003). https://doi.org/10.1016/s0890-5401(03)00088-9

    Article  MathSciNet  MATH  Google Scholar 

  25. Mac Lane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5. Springer, New York (1971). https://doi.org/10.1007/978-1-4612-9839-7

    Book  MATH  Google Scholar 

  26. Milius, S.: Completely iterative algebras and completely iterative monads. Inf. Comput. 196(1), 1–41 (2005). https://doi.org/10.1016/j.ic.2004.05.003

    Article  MathSciNet  MATH  Google Scholar 

  27. Milner, R.: Communication and Concurrency. Prentice-Hall, Upper Saddle River (1989)

    MATH  Google Scholar 

  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). https://doi.org/10.1007/BFb0013462

    Chapter  Google Scholar 

  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). https://doi.org/10.1109/lics.2000.855774

  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). https://doi.org/10.4204/eptcs.66.12

    Article  Google Scholar 

  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). https://doi.org/10.1007/978-3-642-11957-6_26

    Chapter  Google Scholar 

  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). https://doi.org/10.4204/eptcs.32.5

    Article  Google Scholar 

  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). https://doi.org/10.2168/lmcs-11(1:1)2015

    Article  MathSciNet  MATH  Google Scholar 

  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). https://doi.org/10.1007/3-540-45315-6_1

    Chapter  Google Scholar 

  35. Tait, W.W.: Intensional interpretations of functionals of finite type I. J. Symb. Log. 32(2), 198–212 (1967). https://doi.org/10.2307/2271658

    Article  MathSciNet  MATH  Google Scholar 

  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). https://doi.org/10.1109/lics.1997.614955

  37. Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. Informatik, Friedrich-Alexander-Universität Erlangen-Nürnberg, Martensstraße 3, 91058, Erlangen, Germany

    Sergey Goncharov, Christoph Rauch & Lutz Schröder

Authors
  1. Sergey Goncharov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christoph Rauch
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Lutz Schröder
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sergey Goncharov .

Editor information

Editors and Affiliations

  1. Stellenbosch University, Stellenbosch, South Africa

    Bernd Fischer

  2. Reykjavík University, Reykjavik, Iceland

    Tarmo Uustalu

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Goncharov, S., Rauch, C., Schröder, L. (2018). A Metalanguage for Guarded Iteration. In: Fischer, B., Uustalu, T. (eds) Theoretical Aspects of Computing – ICTAC 2018. ICTAC 2018. Lecture Notes in Computer Science(), vol 11187. Springer, Cham. https://doi.org/10.1007/978-3-030-02508-3_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-02508-3_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-02507-6

  • Online ISBN: 978-3-030-02508-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation