University of Cambridge > Talks.cam > Semantics Lunch (Computer Laboratory) > A Concurrent Logical Relation

A Concurrent Logical Relation

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

  • UserJacob Thamsborg (ITU)
  • ClockWednesday 30 May 2012, 14:30-15:30
  • HouseFW26.

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2017 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity