Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6876048 | Theoretical Computer Science | 2015 | 20 Pages |
Abstract
We propose the notion of linear contextual equivalence to formally characterize such program equivalence, as well as a novel and general approach to studying it in higher-order languages, based on labeled transition systems specifically designed for functional languages. We show that linear contextual equivalence indeed coincides with trace equivalence. We illustrate our technique in both deterministic (a linear version of PCF) and non-deterministic (linear PCF in Moggi's framework) functional languages.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Yuxin Deng, Yu Zhang,