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

      Tait in One Big Step

      proceedings-article

      ,

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

      Mathematically Structured Functional Programming

      2 July 2006

      Normalisation, Strong Computability

      Bookmark

            Abstract

            We present a Tait-style proof to show that a simple functional normaliser for a combinatory version of System T terminates. Using a technique pioneered by Bove and Capretta, we can implement the normaliser in total Type Theory. The main interest in our construction is methodological, it is an alternative to the usual small-step operational semantics on the one side and normalisation by evaluation on the other. The present work is motivated by our longer term goal to verify implementations of Type Theory such as Epigram.

            Content

            Author and article information

            Contributors
            Conference
            July 2006
            July 2006
            : 1-10
            Affiliations
            [0001]School of Computer Science and IT, University of Nottingham

            Jubilee Campus, Wollaton Road, Nottingham NG8 1BB, UK
            Article
            10.14236/ewic/MSFP2006.4
            abcabf2f-a4fc-4268-ada0-6190335e8560
            © Thorsten Altenkirch 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
            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