Fold and Unfold for Program Semantics
In this paper we explain how recursion operators can be used to structure and reason about program semantics within a functional language. In particular, we show how the recursion operator fold can be used to structure denotational semantics, how the dual recursion operator unfold can be used to st...
| Main Author: | |
|---|---|
| Format: | Conference or Workshop Item |
| Published: |
1998
|
| Online Access: | https://eprints.nottingham.ac.uk/230/ |
| _version_ | 1848790375221690368 |
|---|---|
| author | Hutton, Graham |
| author_facet | Hutton, Graham |
| author_sort | Hutton, Graham |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | In this paper we explain how recursion operators can be used to structure and reason about program semantics within a functional language. In particular, we show how the recursion operator fold can be used to structure denotational semantics, how the dual recursion operator unfold can be used to structure operational semantics, and how algebraic properties of these operators can be used to reason about program semantics. The techniques are explained with the aid of two main examples, the first concerning arithmetic expressions, and the second concerning Milner's concurrent language CCS. The aim of the paper is to give functional programmers new insights into recursion operators, program semantics, and the relationships between them. |
| first_indexed | 2025-11-14T18:11:37Z |
| format | Conference or Workshop Item |
| id | nottingham-230 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T18:11:37Z |
| publishDate | 1998 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-2302020-05-04T20:33:18Z https://eprints.nottingham.ac.uk/230/ Fold and Unfold for Program Semantics Hutton, Graham In this paper we explain how recursion operators can be used to structure and reason about program semantics within a functional language. In particular, we show how the recursion operator fold can be used to structure denotational semantics, how the dual recursion operator unfold can be used to structure operational semantics, and how algebraic properties of these operators can be used to reason about program semantics. The techniques are explained with the aid of two main examples, the first concerning arithmetic expressions, and the second concerning Milner's concurrent language CCS. The aim of the paper is to give functional programmers new insights into recursion operators, program semantics, and the relationships between them. 1998 Conference or Workshop Item PeerReviewed Hutton, Graham (1998) Fold and Unfold for Program Semantics. In: Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming, September 1998, Baltimore, Maryland. |
| spellingShingle | Hutton, Graham Fold and Unfold for Program Semantics |
| title | Fold and Unfold for Program Semantics |
| title_full | Fold and Unfold for Program Semantics |
| title_fullStr | Fold and Unfold for Program Semantics |
| title_full_unstemmed | Fold and Unfold for Program Semantics |
| title_short | Fold and Unfold for Program Semantics |
| title_sort | fold and unfold for program semantics |
| url | https://eprints.nottingham.ac.uk/230/ |