File:TFPIE2013 Structural Induction Principles.pdf

From tfpie
Revision as of 00:35, 13 May 2013 by Peter88 (talk | contribs) (User defined recursive types are a fundamental feature of modern functional programming languages like Haskell and the ML family of languages. Properties of programs defined by recursion on the structure of a recursive types are generally proved by struct)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
TFPIE2013_Structural_Induction_Principles.pdf(file size: 146 KB, MIME type: application/pdf)

User defined recursive types are a fundamental feature of modern functional programming languages like Haskell and the ML family of languages. Properties of programs defined by recursion on the structure of a recursive types are generally proved by structural induction on the type. It is well known in the theorem proving community how to generate a structural induction principle from the type signature. These methods deserve to be better know in the functional programming community. Existing functional programming textbooks gloss over this material. And yet, if functional programmers do not know how to write down the structural induction principle for a new type - how are they supposed to reason about it? In this paper we describe an algorithm to generate structural induction principles from type signatures. We also discuss how these methods are taught in the Functional Programming course at the University of Wyoming. A Haskell implementation of the algorithm is included in an appendix.

File history

Click on a date/time to view the file as it appeared at that time.

Date/TimeDimensionsUserComment
current00:35, 13 May 2013 (146 KB)Peter88 (talk | contribs)User defined recursive types are a fundamental feature of modern functional programming languages like Haskell and the ML family of languages. Properties of programs defined by recursion on the structure of a recursive types are generally proved by struct
  • You cannot overwrite this file.

The following page links to this file: