Marcelo P. Fiore: Semantic analysis of normalisation by evaluation for typed lambda calculus. PPDP 2002: 26-37