BROADCASTS.com

b'

Also known as the Fundamental Property, this is a theorem stating that for every well-typed term t : T, and every logical relation R between algebraic structures A and B, the meaning of t in A is related by R to the meaning of t in B.\\xa0 I view it as a straightforward semantic soundness property, but where the semantics of types is this somewhat interesting one that interprets types as binary relations on structures A and B.\\xa0 I muse on these matters a bit in the episode.