
Pitts and Stark's nucalculus is a typed lambdacalculus which forms a basis for the study of interaction between higherorder functions and dynamically created names. Logical relations are a powerful tool to prove properties of such a calculus, notably observational equivalence. While Pitts and Stark construct a logical relation for the nucalculus, it is relatively ad hoc and rests heavily on operational aspects of the calculus. We propose an alternative Kripke logical relation for the nucalculus, which is derived naturally from the categorical model of the nucalculus and Mitchell's general notion of Kripke logical relation. This is also related to the Kripke logical relation for the name creation monad by GoubaultLarrecq, Lasota and Nowak (CSL'2002), which the authors claimed had similarities with Pitts and Stark's logical relation. We show that their Kripke logical relation for names is strictly weaker than Pitts and Stark's. We also show that our Kripke logical relation, which extends GoubaultLarrecq, Lasota and Nowak's definition, is equivalent to Pitts and Stark's; our definition rests on purely semantic constituents, and dispenses with the detours through operational semantics that Pitts and Stark use.
© 20022003 Kurt Gödel Society, Norbert Preining. 
20030604
 