30
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Decorated proofs for computational effects: States

      Preprint

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          The syntax of an imperative language does not mention explicitly the state, while its denotational semantics has to mention it. In this paper we show that the equational proofs about an imperative language may hide the state, in the same way as the syntax does.

          Related collections

          Most cited references3

          • Record: found
          • Abstract: not found
          • Article: not found

          Cartesian effect categories are Freyd-categories

            Bookmark
            • Record: found
            • Abstract: found
            • Article: found
            Is Open Access

            Breaking a monad-comonad symmetry between computational effects

            Computational effects may often be interpreted in the Kleisli category of a monad or in the coKleisli category of a comonad. The duality between monads and comonads corresponds, in general, to a symmetry between construction and observation, for instance between raising an exception and looking up a state. Thanks to the properties of adjunction one may go one step further: the coKleisli-on-Kleisli category of a monad provides a kind of observation with respect to a given construction, while dually the Kleisli-on-coKleisli category of a comonad provides a kind of construction with respect to a given observation. In the previous examples this gives rise to catching an exception and updating a state. However, the interpretation of computational effects is usually based on a category which is not self-dual, like the category of sets. This leads to a breaking of the monad-comonad duality. For instance, in a distributive category the state effect has much better properties than the exception effect. This remark provides a novel point of view on the usual mechanism for handling exceptions. The aim of this paper is to build an equational semantics for handling exceptions based on the coKleisli-on-Kleisli category of the monad of exceptions. We focus on n-ary functions and conditionals. We propose a programmer's language for exceptions and we prove that it has the required behaviour with respect to n-ary functions and conditionals.
              Bookmark
              • Record: found
              • Abstract: not found
              • Article: not found

              A formal specification of the Steam-Boiler Control problem by algebraic specifications with implicit state

                Bookmark

                Author and article information

                Journal
                11 December 2011
                2012-09-06
                Article
                10.4204/EPTCS.93.3
                1112.2396
                1ef1a12d-ff45-43ae-9294-bcae6b96368f

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                History
                Custom metadata
                EPTCS 93, 2012, pp. 45-59
                In Proceedings ACCAT 2012, arXiv:1208.4301
                cs.PL cs.LO math.CT
                EPTCS

                Comments

                Comment on this article