This article has not yet been rated on Wikipedia's content assessment scale. It is of interest to the following WikiProjects:

Computing This article is within the scope of WikiProject Computing, a collaborative effort to improve the coverage of computers, computing, and information technology on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.ComputingWikipedia:WikiProject ComputingTemplate:WikiProject ComputingComputing articles ??? This article has not yet received a rating on the project's importance scale.

False claim about normal forms?

I think this is false:

By induction on the structure of types, it follows that if the semantic object S denotes a well-typed term s of type τ, then reifying the object (i.e., ↓^τ S) produces the β-normal η-long form of s

e.g. SYN (app (lam "x" (var "x")) t) where t is some term of basic type. This denotes a well-typed term, yet reifying it does not produce the normal form. It's only after applying meaning that we get a normal form. Can someone confirm? U25506 ( talk) 15:55, 10 May 2011 (UTC) reply

I think "S denotes s" is equivalent to "the meaning of s is S" (and SYN is not a "real" semantic object except for values of base types). Ejrsmi ( talk) 16:47, 10 January 2013 (UTC) reply