857
views
0
recommends
+1 Recommend
1 collections
    0
    shares

      Celebrating 65 years of The Computer Journal - free-to-read perspectives - bcs.org/tcj65

      scite_
       
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

      Verification of Programs on Truly Nested Datatypes in Intensional Type Theory

      proceedings-article
      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
      Bookmark

            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.

            Content

            Author and article information

            Contributors
            Conference
            July 2006
            July 2006
            : 1-12
            Affiliations
            [0001]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
            692124fe-760b-4c18-9c53-112a3f545d1d
            © 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
            History
            Product

            1477-9358 BCS Learning & Development

            Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/MSFP2006.10
            Self URI (journal page): https://ewic.bcs.org/
            Categories
            Electronic Workshops in Computing

            Applied computer science,Computer science,Security & Cryptology,Graphics & Multimedia design,General computer science,Human-computer-interaction
            Terminating Recursion Scheme,Proof Irrelevance,Nested Datatype,Coq,Induction Principle

            Comments

            Comment on this article