[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
