Preprint: Semantic Analysis of Normalisation.

The preprint 

         Semantic Analysis of Normalisation by Evaluation 
                    for Typed Lambda Calculus 

is available from 
        http://www.cl.cam.ac.uk/~mpf23/papers/Types/nbe.ps.gz .

The abstract follows.

   The paper studies normalisation by evaluation for typed lambda 
   calculus from a categorical and algebraic viewpoint.  The first  
   part of the paper analyses the lambda definability result of 
   Jung and Tiuryn via Kripke logical relations and shows how it 
   can be adapted to unify definability and normalisation, yielding 
   an extensional normalisation result.  In the second part of the 
   paper the analysis is refined further by considering intensional 
   Kripke relations (in the form of glueing) and shown to provide 
   a function for normalising terms, casting normalisation by 
   evaluation in the context of categorical glueing. The technical 
   development includes an algebraic treatment of the syntax and 
   semantics of the typed lambda calculus that allows the definition 
   of the normalisation function to be given within a simply typed 

Best, Marcelo.