St Andrews Functional Programming Group

Who are we?

We are the functional programming group at the University of St Andrews. Functional programming involves writing programs using pure functions. Unlike conventional programming (including much object-oriented programming), side-effects are completely eradicated. This allows a very clean, very high-level, very concise programming model.

Functional programs are

Quick to write.

Easy to reason about.

Easy to modify and debug.

Easy to make parallel.

Previous work at St Andrews has focused on Parallel Implementation and Functional Persistence. Our parallel implementation work uses the Glasgow Parallel Haskell dialect of the non-strict functional language Haskell that has been developed in collaboration with researchers at Glasgow, Heriot-Watt and the Open University. Work on functional persistence has been done in collaboration with researchers from UCL and Universidade da Coruña, Spain.

News and Events

The latest St Andrews Functional Programming Group posts from the School of Computer Science blog.

A Type-System for describing System-on-a-Chip Architectures – Jan De Muijnck-Hughes


Event details

  • When: 5th April 2018 12:00 - 13:00
  • Where: Cole 1.33a
  • Format: Talk

Title:

A Type-System for describing System-on-a-Chip Architectures

 

Abstract:

The protocols that describe the interactions between IP Cores on
System-on-a-Chip (SoC) architectures are well-documented. These
protocols described not only the structural properties of the physical
interfaces but also the behaviour of the emanating signals. However,
there is a disconnect between the design of SoC architectures, their
formal description, and the verification of their implementation in
known hardware description languages.

Within the Border Patrol project we are investigating how to capture
and reason about the structural and behavioural properties of SoC
architectures using state-of-the-art advances in programming language
research. Namely, we are investigating using dependent types and
session types to capture and reason about hardware communication.

In this talk I will discuss my work in designing a dependent type-
system and corresponding language that captures and reasons about the
topological structure of a System-on-a-Chip. This language provides
correct-by-construction guarantees over:

1. the physical structure of an interaction protocol;
1. the adherence of a component’s interface to a given protocol; and
1. the validity of the specified connections made between components. 

We provide these guarantees through the (ab)use of dependent types as
presented in Idris; and abuse of indexed monads to reason about
resource usage.

Given time I will give an account of how this language enables
reasoning about SoC behaviour when considered in conjunction with
Session Types.


Diderot: A Parallel Domain-Specific Language for Image Analysis and Visualization – John Reppy


Event details

  • When: 2nd April 2018 13:00 - 14:00
  • Where: Cole 1.33b
  • Format: Seminar

Diderot: A Parallel Domain-Specific Language for Image Analysis and Visualization

Abstract:
The analysis of structure in three-dimensional images is increasingly valuable for biomedical research and computational science. At the same time, the computational burden of processing images is increasing as devices produce images of higher resolution (e.g., typical CT scans have gone from 128^3 to roughly 512^3 resolutions). With the latest scanning technologies, it is also more common for the the values measured at each sample to be multi-dimensional rather than a single scalar, which further complicates implementing mathematically correct methods.

Diderot is a domain-specific language (DSL) for programming advanced 3D image visualization and analysis algorithms. These algorithms, such as volume rendering, fiber tractography, and particle systems, are naturally defined as computations over continuous tensor fields that are reconstructed from the discrete image data. Diderot combines a high-level mathematical programming notation based on tensor calculus with an abstract bulk-synchronous parallelism model. Diderot is designed to both enable rapid prototyping of new image analysis algorithms and high performance on a range of parallel platforms.

In this talk, I will give an overview of the design of Diderot and examples of its use. I will then describe aspects of its implementation with a focus on how we translate the notation of tensor calculus to efficient code. I will also briefly discuss the automated techniques we use to validate the correctness of the compilation process.

Diderot is joint work with Gordon Kindlmann, Charisee Chiw, Lamont Samuels, and Nick Seltzer.

Bio:
John Reppy is a Professor of Computer Science and a Senior Fellow of the Computation Institute at the University of Chicago. He received his Ph.D. from Cornell University in 1992 and spent the first eleven years of his career at Bell Labs in Murray Hill NJ. He has been exploring issues in language design and implementation since the late 1980’s, with a focus on higher-order, typed, functional languages. His work includes the invention of Concurrent ML and work on combining object-oriented and functional language features. His current research is on high-level languages for parallel programming, including the Diderot, Manticore, and Nessie projects.