Program Equivalence in Linear Contexts

Details Program Equivalence in Linear Contexts Program Equivalence in Linear Contexts

2011-06-15

arxiv.org/abs/1106.2872v2

Computer Science

Programming Languages

Technical report, Laboratory for Computer Science, ISCAS

Scientific paper

Program equivalence in linear contexts, where programs are used or executed exactly once, is an important issue in programming languages. However, existing techniques like those based on bisimulations and logical relations only target at contextual equivalence in the usual (non-linear) functional languages, and fail in capturing non-trivial equivalent programs in linear contexts, particularly when non-determinism is present. 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 - it is sound and complete. We illustrate our technique in both deterministic (a linear version of PCF) and non-deterministic (linear PCF in Moggi's framework) functional languages.

Affiliated with

Also associated with

No associations

Rating

Program Equivalence in Linear Contexts does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Program Equivalence in Linear Contexts, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Program Equivalence in Linear Contexts will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-657628