[TYPES] semantic coherence for simply typed lambda-calculus

[Paul B Levy]

Dear all,

Take simply typed lambda-calculus with ->, x, +, 0, 1 types.
Specifically the Curry-style formulation with no type annotations
whatsoever, neither on lambda nor on inl nor on anything else.

Here are the two "coherence" statements I'm interested in.

(1) Any two derivations of Gamma |- M : A have the same denotation.

(2) More generally, for any bicartesian closed category C, any two
derivations of Gamma |- M : A have the same denotation in C.

I can see roughly how to prove these, but before working it out would
like to ask: do these results appear in the literature?  My impression
is that people have studied semantic coherence for fancy languages (e.g.
with subtypes and dependent types), so surely the above statements, or
at least (1), are a simple case of some result in the literature.

Best regards,
Paul



-- 
Paul Blain Levy
School of Computer Science, University of Birmingham
http://www.cs.bham.ac.uk/~pbl