Kevin Hammond

Professor at the University of St Andrews

Kevin Hammond leads the technical effort on Cardano at Input-Output Global (IOG). His research interests lie in programming language design and implementation, with a focus on parallelism and real-time properties of functional languages, including modelling and reasoning about extra-functional properties, using type-based approaches. In total, he has published around 130 research papers, books and articles, and held over 20 national and international research grants, totalling around £11M of research funding, including coordinating several large EU projects. He was a member of the Haskell design committee, co-designed the Hume real-time functional language, and is co-editor of the main reference text on parallel functional programming. targeting heterogeneous parallel architectures. Kevin is a keen hill-walker, whisky connoisseur and enjoys early music. He is interested in how functional programming can be used to improve AI techniques and improve explainability of AI models.

Structured parallelism using nested algorithmic skeletons can greatly ease the task of writing parallel software, since common, but hard-to-debug prob- lems such as race conditions are eliminated by design. However, choosing the right combination of algorithmic skeletons to yield good parallel speedups for a specific program on a specific parallel architecture is still a difficult prob- lem. This work uses the unifying notion of hylomorphisms, a general recursion pattern, to make it possible to reason about both functional correctness prop- erties and extra-functional timing properties of structured parallel programs. We have previously used hylomorphisms to provide a denotational semantics for skeletons, and proved that a given parallel structure for a program sat- isfies functional correctness. This paper expands on this theme, providing a simple operational semantics for algorithmic skeletons, and a cost semantics that can be automatically derived from that operational semantics. We prove both semantics sound with respect to the previous denotational semantics. This means that we can now automatically and statically choose the prov- ably optimal parallel structure for a given program with respect to a parallel architecture or a class of architectures. We are also able to predict speedups using an automatic amortised analysis.

Slides
Video ←Back