Blog
About

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

      Implementing a Normalizer Using Sized Heterogeneous Types

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

      Mathematically Structured Functional Programming

      2 July 2006

      Sized Types, Heterogeneous Types, Nested Types, Interpreter, Normalization, De Bruijn Terms

      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

          In the simply-typed lambda-calculus, a hereditary substitution replaces a free variable in a normal form r by another normal form s of type a, removing freshly created redexes on the fly. It can be defined by lexicographic induction on a and r, thus, giving rise to a structurally recursive normalizer for the simply-typed lambda-calculus. We generalize this scheme to simultaneous substitutions, preserving its simple termination argument. We further implement hereditary simultaneous substitutions in a functional programming language with sized heterogeneous inductive types, F ŵ, arriving at an interpreter whose termination can be tracked by the type system of its host programming language.

          Related collections

          Most cited references 10

          • Record: found
          • Abstract: not found
          • Book Chapter: not found

          Monadic Presentations of Lambda Terms Using Generalized Inductive Types

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

            de Bruijn notation as a nested datatype

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

              Inductive types and type constraints in the second-order lambda calculus

               Nax Mendler (1991)
                Bookmark

                Author and article information

                Contributors
                Conference
                July 2006
                July 2006
                : 1-12
                Affiliations
                Institut für Informatik, Ludwig-Maximilians-Universität München

                Oettingenstr. 67, D-80538 München, Germany
                Article
                10.14236/ewic/MSFP2006.3
                © Andreas Abel. 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