Tait in One Big Step

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.

Contributors

Thorsten Altenkirch

James Chapman

Conference

Publication date: July 2006

Publication date (Print): July 2006

Pages: 1-10

Affiliations

School of Computer Science and IT, University of Nottingham

Jubilee Campus, Wollaton Road, Nottingham NG8 1BB, UK

Article

DOI: 10.14236/ewic/MSFP2006.4

Copyright statement: © Thorsten Altenkirch et al. Published by BCS Learning and Development Ltd. Workshop on Mathematically Structured Functional Programming (MSFP 2006), Kuressaare, Estonia

License:

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/

Conference name: Workshop on Mathematically Structured Functional Programming (MSFP 2006)

Conference acronym: MSFP

Conference number:

Conference location: Kuressaare, Estonia

Conference date: 2 July 2006

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: Mathematically Structured Functional Programming

Product

Product Information: 1477-9358BCS Learning & Development

Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/MSFP2006.4

Self URI (journal page): https://ewic.bcs.org/

Categories

Series title: Electronic Workshops in Computing