On Completeness of Logical Relations for Monadic Types

Details On Completeness of Logical Relations for Monadic Types On Completeness of Logical Relations for Monadic Types

2006-12-21

arxiv.org/abs/cs/0612106v1

Advances in Computer Science - ASIAN 2006, Secure Software, 11th Asian Computing Science Conference, Tokyo, Japan, December 6-

Computer Science

Logic in Computer Science

20 pages, full version of the paper published at ASIAN'2006, with the same title

Scientific paper

10.1007/978-3-540-77505-8_17

Software security can be ensured by specifying and verifying security properties of software using formal methods with strong theoretical bases. In particular, programs can be modeled in the framework of lambda-calculi, and interesting properties can be expressed formally by contextual equivalence (a.k.a. observational equivalence). Furthermore, imperative features, which exist in most real-life software, can be nicely expressed in the so-called computational lambda-calculus. Contextual equivalence is difficult to prove directly, but we can often use logical relations as a tool to establish it in lambda-calculi. We have already defined logical relations for the computational lambda-calculus in previous work. We devote this paper to the study of their completeness w.r.t. contextual equivalence in the computational lambda-calculus.

Affiliated with

Also associated with

No associations

Rating

On Completeness of Logical Relations for Monadic Types 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 On Completeness of Logical Relations for Monadic Types, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On Completeness of Logical Relations for Monadic Types will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-21833