Blog
About

117
views
0
recommends
+1 Recommend
1 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

      Verification of Programs on Truly Nested Datatypes in Intensional Type Theory

      Workshop on Mathematically Structured Functional Programming (MSFP 2006) (MSFP)

      Mathematically Structured Functional Programming

      2 July 2006

      Nested Datatype, Induction Principle, Terminating Recursion Scheme, Proof Irrelevance, Coq

      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

          Nested datatypes are families of datatypes that are indexed over all types such that the constructors may relate different family members (unlike the homogeneous lists). Moreover, even the family name may be involved in the expression that gives the index the argument type of the constructor refers to. Especially in this case of true nesting, termination of functions that traverse these data structures is far from being obvious. A joint article with A. Abel and T. Uustalu (TCS 333(1–2), pp. 3–66, 2005) proposes iteration schemes that guarantee termination not by structural requirements but just by polymorphic typing. And they are generic in the sense that no specific syntactic form of the underlying datatype “functor” is required. However, there have not been induction principles for the verification of the programs thus obtained although they are well-known in the usual model of initial algebras on endofunctor categories.

          The new contribution is a representation of nested datatypes in intensional type theory (more specifically, in the Calculus of Inductive Constructions) that is still generic, guarantees termination of all expressible programs and has induction principles that allow to prove functoriality of monotonicity witnesses (maps for nested datatypes) and naturality properties of iteratively defined polymorphic functions.

          Related collections

          Most cited references 6

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

          de Bruijn notation as a nested datatype

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

            A general formulation of simultaneous inductive-recursive definitions in type theory

             Peter Dybjer (2000)
            The first example of a simultaneous inductive-recursive definition in intuitionistic type theory is Martin-Löfs universe à la Tarski. A set U0 of codes for small sets is generated inductively at the same time as a function T0, which maps a code to the corresponding small set, is defined by recursion on the way the elements of U0 are generated.
              Bookmark
              • Record: found
              • Abstract: not found
              • Article: not found

              Iteration and coiteration schemes for higher-order and nested datatypes

                Bookmark

                Author and article information

                Contributors
                Conference
                July 2006
                July 2006
                : 1-12
                Affiliations
                I.R.I.T., Université Paul Sabatier & C.N.R.S.

                118 route de Narbonne, F-31062 Toulouse Cedex 9, France
                Article
                10.14236/ewic/MSFP2006.10
                © Ralph Matthes et al. Published by BCS Learning and Development Ltd. Workshop on Mathematically Structured Functional Programming (MSFP 2006), Kuressaare, Estonia

                This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

                Workshop on Mathematically Structured Functional Programming (MSFP 2006)
                MSFP
                Kuressaare, Estonia
                2 July 2006
                Electronic Workshops in Computing (eWiC)
                Mathematically Structured Functional Programming
                Product
                Product Information: 1477-9358BCS Learning & Development
                Self URI (journal page): https://ewic.bcs.org/
                Categories
                Electronic Workshops in Computing

                Comments

                Comment on this article