<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
@INPROCEEDINGS{PittsAM:obspho,
 AUTHOR={A.~M.~Pitts and I.~D.~B.~Stark},
 TITLE={On the Observable Properties of Higher Order Functions That
 Dynamically Create Local Names (Preliminary Report)},
 BOOKTITLE={Workshop on State in Programming Languages, {Copenhagen},
 1993}, 
 ORGANIZATION={ACM SIGPLAN},
 NOTE={Yale Univ.\ Dept.\ Computer Science Technical Report
 YALEU/DCS/RR-968}, 
 YEAR=1993,
 PAGES={31--45},
 ABSTRACT={The research reported in this paper is concerned with the
 problem of reasoning about properties of higher order functions
 involving state.  It is motivated by the desire to identify what, if
 any, are the difficulties created purely by {\em locality\/} of
 state, independent of other properties such as side-effects,
 exceptional termination and non-termination due to recursion. We
 consider a simple language (equivalent to a fragment of Standard ML)
 of typed, higher order functions that can dynamically create fresh
 {\em names}. Names are created with local scope, can be tested for
 equality and can be passed around via function application, but that
 is all.\par We demonstrate that despite the simplicity of the
 language and its operational semantics, the observable properties of
 such functions can be very subtle. Two methods are introduced for
 analyzing Morris-style observational equivalence between expressions
 in the language. The first method introduces a notion of
 `applicative' equivalence incorporating a syntactic version of
 O'Hearn and Tennent's relationally parametric functors and a version
 of {\em representation independence\/} for local names. This
 applicative equivalence is properly contained in the relation of
 observational equivalence, but coincides with it for first order
 expressions (and is decidable there). The second method develops a
 general, categorical framework for computationally adequate models of
 the language, based on Moggi's {\em monadic\/} approach to
 denotational semantics. We give examples of models, one of which is
 fully abstract for first order expressions.  No fully abstract
 (concrete) model of the whole language is known.}}