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.

2 Responses to “Normalisation for Typed Combinatory Logic”

  1. Sebastian Hanowski Says:

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

  2. Thorsten Says:

    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