Tait in One Big Step | Zendy

Thorsten Altenkirch | Zendy; James Chapman | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Tait in One Big Step

Author(s) -

Thorsten Altenkirch,

James Chapman

Publication year - 2006

Publication title -

electronic workshops in computing

Language(s) - English

Resource type - Conference proceedings

ISSN - 1477-9358

DOI - 10.14236/ewic/msfp2006.4

Subject(s) - implementation , semantics (computer science) , computer science , simple (philosophy) , style (visual arts) , term (time) , programming language , type theory , type (biology) , operational semantics , theoretical computer science , philosophy , epistemology , literature , art , ecology , physics , quantum mechanics , biology

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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research