[TYPES] semantics of `quote'

[Thomas Streicher]

Does anyone know of a reference to work on (denotational) semantics of
`quote' constructs in functional languages like LISP?

Probably there is nothing like that since the operational evaluation rule

     quote M -> "M"   (where "M" is e.g. a Goedel number for M)

induces an onservational equivalence coinciding with syntactic equality.
Well, there should be variants if quote is call-by-value where the meaning
of quote M is a Goedel number of the weak head normal form of M.

More generally, one might ask for quote constructs  \libqu  where
\libqu M -> "N" such that M and N have the same denotation (whatever this is).

The reason why I am asking this on TYPES is that languages with (a kind of)
quote seem to be necessary for constructing realizabilty models of Martin-Loef
type theory validating Church's Thesis

    (\Pi f : N \to N) (\Sigma e : N) (\Pi n:N) {e}(n) = f(n)

a question brought up recently by M.Maietti and G. Sambin.

My impression is that a quote construct seems to be incompatible with
the \xi-rule
                    M = N
                 -------------
                  \x.M = \x.N

Best regards, Thomas