Library support for Idris

Idris is a functional programming language developed at the University of St Andrews (and elsewhere). It has similarities with Haskell (taught as part of CS2006) but additionally has a more expressive type system which allows programmers to state properties of programs which are checkable at compile time, such as assumptions about sizes of data structures, […]

Continue reading

Trustworthy Refactoring in Idris

Refactoring is the process of changing the structure of a program without modifying its behaviour, or functional semantics. Often, refactoring tools are implemented and then the correctness of the transformations is demonstrated correct by vigorous testing or well-formed rewrite rules that the implementation is based on. However, most programming languages do not have a well-formed […]

Continue reading

Parallel Skeletons in Erlang

Parallel Skeletons are generalised higher-order functions for abstracting over the low-level complexities of implementing common parallel algorithmic behaviours. The Skel library (https://skel.weebly.com) is a parallel skeleton library for Erlang, offering a domain specific language (DSL) allowing Erlang programers to write parallel programs quickly and easily.   The focus of this project is to add new […]

Continue reading