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

      Intersection types for unbind and rebind

      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

          We define a type system with intersection types for an extension of lambda-calculus with unbind and rebind operators. In this calculus, a term with free variables, representing open code, can be packed into an "unbound" term, and passed around as a value. In order to execute inside code, an unbound term should be explicitly rebound at the point where it is used. Unbinding and rebinding are hierarchical, that is, the term can contain arbitrarily nested unbound terms, whose inside code can only be executed after a sequence of rebinds has been applied. Correspondingly, types are decorated with levels, and a term has type decorated with k if it needs k rebinds in order to reduce to a value. With intersection types we model the fact that a term can be used differently in contexts providing different numbers of unbinds. In particular, top-level terms, that is, terms not requiring unbinds to reduce to values, should have a value type, that is, an intersection type where at least one element has level 0. With the proposed intersection type system we get soundness under the call-by-value strategy, an issue which was not resolved by previous type systems.

          Related collections

          Most cited references 11

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

          LCF considered as a programming language

           G.D. Plotkin (1977)
            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            MetaML and multi-stage programming with explicit annotations

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

              An extension of the basic functionality theory for the $\lambda$-calculus.

                Bookmark

                Author and article information

                Journal
                23 January 2011
                Article
                10.4204/EPTCS.45.4
                1101.4426

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

                Custom metadata
                EPTCS 45, 2011, pp. 45-58
                In Proceedings ITRS 2010, arXiv:1101.4104
                cs.LO cs.PL
                EPTCS

                Comments

                Comment on this article