Please use this identifier to cite or link to this item:
|Title:||Completeness of Bisimilarity for Contextual Equivalence in Linear Theories.|
|Authors:||Crole, R. L.|
|Citation:||Logic Journal of the IGPL, 2001, 9 (1), pp.27-51|
|Abstract:||In this paper, we develop new variations of methods from operational semantics, and show how to apply these to a linear type theory which has a lazy operational semantics. In particular, we consider how one can establish contextual equivalences in a linear theory with function types and tensor types by instead establishing bisimulations. Thus bisimilarity is sound for contextual equivalence. Further, we show that bisimilarity is complete for contextual equivalence. We shall show that the notion of a program context in the linear setting is non-trivial. In particular, we give a definition of linear context which is amenable to mechanization in a theorem prover, and explain why a more naive approach to dealing with linear contexts would not be so tractable. The central contributions of the paper are: the formulation, in a linear setting, of a good notion of program context and the associated contextual equivalence; an adaptation of Howe's method; the notion of a linear precongruence; and a proof that bisimilarity is sound and complete for contextual equivalence.|
|Appears in Collections:||Published Articles, Dept. of Computer Science|
Files in This Item:
There are no files associated with this item.
Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.