[Prev][Next][Index][Thread]
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
meta-theory.
Best, Marcelo.