415
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

      proceedings-article

      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

      Bookmark

            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.

            Content

            Author and article information

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

            Oettingenstr. 67, D-80538 München, Germany
            Article
            10.14236/ewic/MSFP2006.3
            f65583c4-8a42-4b79-92c4-a186f6409503
            © 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