[Prev][Next][Index][Thread]

a full abstraction result for local variables



The following TechReport is now available by anonymous ftp:

  "Full Abstraction for the Second Order Subset of an Algol-like
   Language (Preliminary Report)"
   by: Kurt Sieber, University Saarbr"ucken


ftp-server: laurel.cs.uni-sb.de (134.96.224.176)
directory:  pub/sieber
files:      94_fa2ndalg.ps.Z   or  94_fa2ndalg.dvi.Z


Abstract:

The search for fully abstract models of block structured languages
with local variables began in the mid 80s.  A series of observational
congruences in [MeyerS88] revealed the shortcomings of existing
models and served as test cases for new ones.  The most recently
developed models in [OHearnT93, Sieber93] could prove all these
test equivalences, but it was not known whether they are fully
abstract.  In this paper we show that (a slight variant of) the model
in [Sieber93] IS fully abstract for the second order subset of an
ALGOL-like language (which subsumes all the test equivalences).  

The general technique for constructing our model is still the same as
in [MeyerS88], namely we use `relationally structured locally
complete partial orders' with `relation preserving locally continuous
functions'.  The particular model differs from the one in
[MeyerS88] by having the `finest possible relation structure', an
idea which we have developed in [Sieber92] for constructing a fully
abstract model for the second order subset of sequential PCF.  The
full abstraction proof also uses some ideas from [Sieber92], but for
its main part we had to develop new techniques in order to cope with
the more complicated (in comparison with PCF) setting of an ALGOL-like
language. 

@InProceedings{MeyerS88,
  author = 	"Albert R. Meyer and Kurt Sieber",
  title = 	"Towards Fully Abstract Semantics for Local Variables:
		 Preliminary Report",   
  booktitle = 	"Proc.\ $15^{th}$ Annual {ACM} Symp. on Principles of
		 Programming Languages",
  year = 	"1988",
  pages = 	"191--203",
  address =     "San Diego"
}

@inproceedings{OHearnT93,
	AUTHOR = {Peter W. O'Hearn and Robert D. Tennent},
	TITLE = {Relational Parametricity and Local Variables},
	BOOKTITLE = {Proc. $20^{th}$ Annual {ACM} Symposium on Principles 
        	     of Programming Languages},
	PAGES = {171--184},
	YEAR = {1993}
}

@InProceedings{Sieber92,
  author = 	"Kurt Sieber",
  title = 	"Reasoning about sequential functions via logical relations",
  booktitle = 	"Proc. {LMS} Symposium on Applications of Categories
		 in Computer Science, Durham 1991",
  year = 	"1992",
  editor = 	"M. P. Fourman and P. T. Johnstone and A. M. Pitts",
  pages = 	"258--269",
  publisher = 	"Cambridge University Press",
  series =      "{LMS} Lecture Note Series 177"
}

@inproceedings{Sieber93,
	AUTHOR = {Kurt Sieber},
	TITLE = {New Steps Towards Full Abstraction for Local Variables},
	BOOKTITLE = {Proc. ACM SIGPLAN Workshop on State in
                     Programming Languages (Technical Report
                     YALEU/DCS/RR-968, Yale University)},     
        ADDRESS = {Copenhagen, Denmark},
	PAGES = {88--100},
	YEAR = {1993}
}