Speculative execution is an important technique that has historically been used to extract concurrency from sequential programs. While techniques to support speculation work well ...
Lukasz Ziarek, Suresh Jagannathan, Matthew Fluet, ...
With the emergence of commodity multicore architectures, exploiting tightly-coupled parallelism has become increasingly important. Functional programming languages, such as Haskel...
Abdallah Al Zain, Kevin Hammond, Jost Berthold, Ph...
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...
Jade Alglave, Anthony C. J. Fox, Samin Ishtiaq, Ma...
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...
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...
Transactional memory (TM) provides a safer, more modular, and more scalable alternative to traditional lock-based synchronization. Implementing high performance TM systems has rec...
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 ...
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 ...
Mitchell's notion of representation independence is a particularly useful application of Reynolds' relational parametricity -- two different implementations of an abstra...
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...
Jeremy Condit, Brian Hackett, Shuvendu K. Lahiri, ...