POPL
2009
ACM
13 years 11 months ago
2009
ACM
Speculative execution is an important technique that has historically been used to extract concurrency from sequential programs. While techniques to support speculation work well ...
POPL
2009
ACM
13 years 11 months ago
2009
ACM
With the emergence of commodity multicore architectures, exploiting tightly-coupled parallelism has become increasingly important. Functional programming languages, such as Haskel...
POPL
2009
ACM
13 years 11 months ago
2009
ACM
We develop a rigorous semantics for Power and ARM multiprocessor programs, including their relaxed memory model and the behaviour of reasonable fragments of their instruction sets...
POPL
2009
ACM
13 years 11 months ago
2009
ACM
Haskell has a rich set of synchronization primitives for implemented-state concurrency abstractions, ranging from the very high level (Software Transactional Memory) to the very l...
POPL
2009
ACM
13 years 11 months ago
2009
ACM
Concurrent Collections (CnC)[8] is a declarative parallel language that allows the application developer to express their parallel application as a collection of high-level comput...
POPL
2009
ACM
13 years 11 months ago
2009
ACM
Transactional memory (TM) provides a safer, more modular, and more scalable alternative to traditional lock-based synchronization. Implementing high performance TM systems has rec...
POPL
2009
ACM
14 years 5 months ago
2009
ACM
This work develops an integrated approach to the verification of behaviourally rich programs, founded directly on operational semantics. The power of the approach is demonstrated ...
POPL
2009
ACM
14 years 5 months ago
2009
ACM
In this paper, we show how pattern matching can be seen to arise from a proof term assignment for the focused sequent calculus. This use of the Curry-Howard correspondence allows ...
POPL
2009
ACM
14 years 5 months ago
2009
ACM
Mitchell's notion of representation independence is a particularly useful application of Reynolds' relational parametricity -- two different implementations of an abstra...
POPL
2009
ACM
14 years 5 months ago
2009
ACM
We present a unified approach to type checking and property checking for low-level code. Type checking for low-level code is challenging because type safety often depends on compl...