A Metalanguage for Guarded Iteration

Sergey Goncharov; Christoph Rauch; Lutz Schröder

doi:10.1007/978-3-030-02508-3_11

A Metalanguage for Guarded Iteration

Sergey Goncharov^*
, Christoph Rauch
, Lutz Schröder

^*Corresponding author for this work

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	Theoretical Aspects of Computing – ICTAC 2018 - 15th International Colloquium, 2018, Proceedings
Editors	Bernd Fischer, Tarmo Uustalu, Tarmo Uustalu
Publisher	Springer Verlag
Pages	191-210
Number of pages	20
ISBN (Print)	9783030025076
DOIs	https://doi.org/10.1007/978-3-030-02508-3_11
Publication status	Published - 2018
Event	15th International Colloquium on Theoretical Aspects of Computing, ICTAC 2018 - Stellenbosch, South Africa Duration: 16 Oct 2018 → 19 Oct 2018

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	11187 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	15th International Colloquium on Theoretical Aspects of Computing, ICTAC 2018
Country/Territory	South Africa
City	Stellenbosch
Period	16/10/18 → 19/10/18

Bibliographical note

Publisher Copyright:
© 2018, Springer Nature Switzerland AG.

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-030-02508-3_11

Cite this

Goncharov, S., Rauch, C., & Schröder, L. (2018). A Metalanguage for Guarded Iteration. In B. Fischer, T. Uustalu, & T. Uustalu (Eds.), Theoretical Aspects of Computing – ICTAC 2018 - 15th International Colloquium, 2018, Proceedings (pp. 191-210). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11187 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-030-02508-3_11

Goncharov, Sergey ; Rauch, Christoph ; Schröder, Lutz. / A Metalanguage for Guarded Iteration. Theoretical Aspects of Computing – ICTAC 2018 - 15th International Colloquium, 2018, Proceedings. editor / Bernd Fischer ; Tarmo Uustalu ; Tarmo Uustalu. Springer Verlag, 2018. pp. 191-210 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{4c6e2bea9ef44237b374534b60dec95b,

title = "A Metalanguage for Guarded Iteration",

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.",

author = "Sergey Goncharov and Christoph Rauch and Lutz Schr{\"o}der",

note = "Publisher Copyright: {\textcopyright} 2018, Springer Nature Switzerland AG.; 15th International Colloquium on Theoretical Aspects of Computing, ICTAC 2018 ; Conference date: 16-10-2018 Through 19-10-2018",

year = "2018",

doi = "10.1007/978-3-030-02508-3\_11",

language = "English",

isbn = "9783030025076",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "191--210",

editor = "Bernd Fischer and Tarmo Uustalu and Tarmo Uustalu",

booktitle = "Theoretical Aspects of Computing – ICTAC 2018 - 15th International Colloquium, 2018, Proceedings",

}

Goncharov, S, Rauch, C & Schröder, L 2018, A Metalanguage for Guarded Iteration. in B Fischer, T Uustalu & T Uustalu (eds), Theoretical Aspects of Computing – ICTAC 2018 - 15th International Colloquium, 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11187 LNCS, Springer Verlag, pp. 191-210, 15th International Colloquium on Theoretical Aspects of Computing, ICTAC 2018, Stellenbosch, South Africa, 16/10/18. https://doi.org/10.1007/978-3-030-02508-3_11

A Metalanguage for Guarded Iteration. / Goncharov, Sergey; Rauch, Christoph; Schröder, Lutz.
Theoretical Aspects of Computing – ICTAC 2018 - 15th International Colloquium, 2018, Proceedings. ed. / Bernd Fischer; Tarmo Uustalu; Tarmo Uustalu. Springer Verlag, 2018. p. 191-210 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11187 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - A Metalanguage for Guarded Iteration

AU - Goncharov, Sergey

AU - Rauch, Christoph

AU - Schröder, Lutz

PY - 2018

Y1 - 2018

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/85055444035

U2 - 10.1007/978-3-030-02508-3_11

DO - 10.1007/978-3-030-02508-3_11

M3 - Conference contribution

AN - SCOPUS:85055444035

SN - 9783030025076

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 191

EP - 210

BT - Theoretical Aspects of Computing – ICTAC 2018 - 15th International Colloquium, 2018, Proceedings

A2 - Fischer, Bernd

A2 - Uustalu, Tarmo

PB - Springer Verlag

T2 - 15th International Colloquium on Theoretical Aspects of Computing, ICTAC 2018

Y2 - 16 October 2018 through 19 October 2018

ER -

Goncharov S, Rauch C, Schröder L. A Metalanguage for Guarded Iteration. In Fischer B, Uustalu T, Uustalu T, editors, Theoretical Aspects of Computing – ICTAC 2018 - 15th International Colloquium, 2018, Proceedings. Springer Verlag. 2018. p. 191-210. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-02508-3_11

A Metalanguage for Guarded Iteration

Abstract

Publication series

Conference

Bibliographical note

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this