![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Jacob Thamsborg (ITU)
Wednesday 30 May 2012, 14:30-15:30
A Concurrent Logical Relation
- đ¤ Speaker: Jacob Thamsborg (ITU)
- đ Date & Time: Wednesday 30 May 2012, 14:30 - 15:30
- đ Venue: FW26
Abstract
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.
Series This talk is part of the Semantics Lunch (Computer Laboratory) series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Department of Computer Science and Technology talks and seminars
- FW26
- Interested Talks
- Martin's interesting talks
- School of Technology
- Semantics Lunch (Computer Laboratory)
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.