Speaker: David Castro, University of St Andrews

Title: Reasoning about Structured Parallel Processes using Types and
Hylomorphisms

Abstract:

The increasing importance of parallelism has motivated the creation of
better abstractions for writing parallel software, such as structured
parallelism using nested algorithmic skeletons. However, statically
choosing a combination of algorithmic skeletons that yield good
speedups when compared with a manually optimised solution remains a
difficult task. In order to do so, it is crucial to be able to
simultaneously reason about both the cost of, and semantic
equivalences between different parallel structures. In this talk, I
will present a new type-based mechanism for reasoning about these
properties, focusing on the introduction of parallelism to a
specification of the functional behaviour of a program. This mechanism
exploits well-known properties of a very general recursion pattern,
hylomorphisms, and a denotational semantics for structured parallel
processes described in terms of hylomorphisms. Using this approach, it
is possible to determine formally whether it is possible to introduce
a desired parallel structure to a program without altering its
functional behaviour, and choose a structure that minimises some
parameter cost model.