542
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

      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
            History
            Product

            1477-9358 BCS Learning & Development

            Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/MSFP2006.3
            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
            Normalization,De Bruijn Terms,Sized Types,Heterogeneous Types,Nested Types,Interpreter

            Comments

            Comment on this article