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

      Relating Church-Style and Curry-Style Subtyping

      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

          Type theories with higher-order subtyping or singleton types are examples of systems where computation rules for variables are affected by type information in the context. A complication for these systems is that bounds declared in the context do not interact well with the logical relation proof of completeness or termination. This paper proposes a natural modification to the type syntax for F-Omega-Sub, adding variable's bound to the variable type constructor, thereby separating the computational behavior of the variable from the context. The algorithm for subtyping in F-Omega-Sub can then be given on types without context or kind information. As a consequence, the metatheory follows the general approach for type systems without computational information in the context, including a simple logical relation definition without Kripke-style indexing by context. This new presentation of the system is shown to be equivalent to the traditional presentation without bounds on the variable type constructor.

          Related collections

          Most cited references5

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

          On equivalence and canonical forms in the LF type theory

            Bookmark
            • Record: found
            • Abstract: not found
            • Conference Proceedings: not found

            Toward a typed foundation for method specialization and inheritance

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

              A semantic basis for Quest

                Bookmark

                Author and article information

                Journal
                23 January 2011
                Article
                10.4204/EPTCS.45.1
                1101.4423
                f31b292e-86dd-4ae4-80a6-1b447aba443c

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

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

                Comments

                Comment on this article