by James Chapman on March 14, 2006.
Tagged as: Lunches.
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.