We present work-in-progress on RTG, a domain specific language embedded in Haskell designed to explore the affordances of geometry as a means to generate and manipulate rhythmic patterns in live coded music. Examples of how simple geometry is capable of ...

This paper describes the design of a verified tool for analyzing tool paths defined in the RS-274 language for 3D printing systems. We describe how the analyzer was designed to allow a mixture of verification and code-extraction techniques to be combined ...

Functional programming in the small works great. Things start to get shaky when there are many services and teams involved, something that is becoming more and more common with large distributed systems.

This paper compares OpenCL, CUDA, and HIP as compilation targets for Futhark, a functional array language. We compare the performance of OpenCL versus CUDA, and OpenCL versus HIP, on the code generated by the Futhark compiler on a collection of 48 ...

We present a case-study of using functional programming in the real world at a very large scale. At Standard Chartered Bank, Haskell is used in a core software library supporting the entire Markets division -- a business line with 3 billion USD operating ...

Producing efficient array code is crucial in high-performance domains like image processing and machine learning. It requires the ability to control factors like compute intensity and locality by reordering computations into different stages and ...

One of the central claims of fame of the Coq proof assistant is extraction, i.e. the ability to obtain efficient programs in industrial programming languages such as OCaml, Haskell, or Scheme from programs written in Coq’s expressive dependent type ...

Modular design is critical in reducing hardware designer's cognitive load and development cost. However, it is challenging to modularize high-performance pipelined circuits with structural, data, and control hazards because their resolution---stalling, ...

Language model-based code completion models have quickly grown in use, helping thousands of developers write code in many different programming languages. However, research on code completion models typically focuses on imperative languages such as ...

The use of functional constructs in programming languages such as Python has been advocated to help write more concise source code, improve parallelization, and reduce side effects. Nevertheless, their usage could lead to understandability issues. This ...

Energy efficiency is a growing concern for software developers. This empirical study investigates the impact of compiler optimizations on energy efficiency in Haskell programs compiled using the Glasgow Haskell Compiler (GHC). We focus on GHC's -O2 ...

Inlining is a crucial optimisation when compiling functional programming languages. This paper describes how we have implemented and verified function inlining and loop specialisation for PureCake, a verified compiler for a Haskell-like (purely ...

Accelerating programs is typically done by recognizing code idioms matching high-performance libraries or hardware interfaces. However, recognizing such idioms automatically is challenging. The idiom recognition machinery is difficult to write and ...

We present a hardware implementation of the high-level multi-paradigm language OCaml using a declarative language called Eclat. Eclat is tailored for programming reactive hardware applications mixing interaction with physical devices and long-...

Many programs which solve complicated problems can be seen as inversions of other, much simpler, programs. One particular example is transforming verifiers into solvers, which can be achieved with low effort by implementing the verifier in a relational ...

We show how the basic Combinatory Homomorphic Automatic Differentiation (CHAD) algorithm can be optimised, using well-known methods, to yield a simple, composable, and generally applicable reverse-mode automatic differentiation (AD) technique that has ...

In this paper, methods for increasing the efficiency of VLSI development based on the method of architecture-independent design are proposed. The route of high-level VLSI synthesis is considered. The principle of constructing a VLSI hardware model ...

BSML is a pure functional library for the multi-paradigm language OCaml. BSML embodies the principles of the Bulk Synchronous Parallel (BSP) model, a model of scalable parallel computing. We propose a formalization of BSML primitives with WhyML, ...

Information Flow Control (IFC) in dynamic contexts is challenging due to different interpretations of security that arise. This paper introduces a modular framework to address this challenge. We present a dynamic floating-label enforcement mechanism ...

This paper presents stableKanren, a miniKanren extension with normal logic programming support under stable model semantics. MiniKanren is a relational programming solver implemented atop Scheme via shallow embedding, which means the predicate in each ...