A Concurrent Logical Relation

Add to your list(s) Download to your calendar using vCal

• Jacob Thamsborg (ITU)
• Wednesday 30 May 2012, 14:30-15:30
• FW26.

If you have a question about this talk, please contact Peter Sewell.

NB: changed (again!) unusual day/time

I’ll present recent work on a logical relation for showing the correctness of program transformations based on a new type-and-effect system for a concurrent extension of an ML-like language.

We’ll see how to use the model to verify interesting program transformations that rely on effect annotations. In particular, I’ll explain a Parallelization Theorem, which expresses when it is sound to run two expressions in parallel instead of sequentially. The conditions are expressed solely in terms of the types and effects of the expressions. To the best of our knowledge, this is the first such result for a concurrent higher-order language with higher-order store and dynamic memory allocation.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.