«
»

Normalisation for Typed Combinatory Logic

March 14th, 2006 by James Chapman

I presented a normalisation proof for typed combinatory logic via normalisation by evaluation/reduction-free normalisation/normalisation by intuitionistic model construction. Whilst this is certainly not news it represents a clear and simple example of the technique. It is very natural to consider a type theory such as Epigram’s as the metalanguage and therein lies some of the appeal. More detail to follow.

This entry was posted on Tuesday, March 14th, 2006 at 1:12 am and is filed under Lunches. You can follow any responses to this entry through the RSS 2.0 feed. You can skip to the end and leave a response. Pinging is currently not allowed.

2 Responses to “Normalisation for Typed Combinatory Logic”

  1. Sebastian Hanowski Says:
    March 14th, 2006 at 10:56 am

    I’d like to know if you make reference to Thorstens Normalisation by Completeness.

  2. Thorsten Says:
    March 17th, 2006 at 10:24 am

    Hi Sebastian,

    you are a bit ahead… Since we are only combinatoric in the moment, the logical connection is less clear. The construction James presented is the one from Coquand’s and Dybjer’s paper on mechanical normalisation. It can also be directed related to Tait’s normalisation proof. I hope James writes this up soon…

    Cheers,
    Thorsten

Leave a Reply